nach oben

Journal of Automated Reasoning

Erschienen in:

30.05.2017

Translation of IEC 61131-3 Function Block Diagrams to PVS for Formal Verification with Real-Time Nuclear Application

verfasst von: Josh Newell, Linna Pang, David Tremaine, Alan Wassyng, Mark Lawford

Erschienen in: Journal of Automated Reasoning | Ausgabe 1/2018

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

The trip computers for the two reactor shutdown systems of the Ontario Power Generation (OPG) Darlington Nuclear Power Generating Station are being refurbished due to hardware obsolescence. For one of the systems, the general purpose computer originally used is being replaced by a programmable logic controller (PLC). The trip computer application software has been rewritten using function block diagrams (FBDs), a commonly used PLC programming language defined in the IEC 61131-3 standard. The replacement project’s quality assurance program requires that formal verification be performed to compare the FBDs against a formal software requirements specification written using tabular expressions (TEs). The PVS theorem proving tool is used in formal verification. Custom tools developed for OPG are used to translate TEs and FBDs into PVS code. In this paper, we present a method to rigorously translate the graphical FBD language to a mathematical model in PVS using an abstract syntax to represent the FBD constructs. We use an example from the replacement project to demonstrate the use of the model to translate a FBD module into a PVS specification. We then extend that example to demonstrate the method’s applicability to a Simulink-based design.

Vorheriger Artikel Safe Autonomy Under Perception Uncertainty Using Chance-Constrained Temporal Logic

Nächster Artikel Towards Probabilistic Formal Analysis of SATS-Simultaneously Moving Aircraft (SATS-SMA)

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

This paper is an extension of [11] and contains a more extensive example that includes timer functions, a strategy for discharging consistency proofs in PVS, and an application of the methodology, using the same example, with Simulink.

A small portion of the software design is written using structured text (ST), but that is not relevant to the subject of this paper.

The use of IEC 61131-3 compliant built-in FBs was based on a formal specification and subsequent verification of their behaviour; one of many PLC qualification activities.

A FBD design is consistent if for every input it produces an expected output. Otherwise, a FBD design trivially satisfies any requirement.

The prefixes in this section refer to monitored variables (m_...), controlled variables (c_...), enumerations (e_...), constants (k_...) and functions (f_...).

Concrete examples are available to assist the reader with the translation rules (Sects. 3, 4 and 5) at http://www.swi.com/research/NFM2016.

The application expression consists of the block name applied with ordered arguments. An example of a PVS application expression is MOVE( input, output ) where MOVE is the block name, and input and output are the arguments.

Timer TON (On-delay) is commonly used as a component of safety-critical systems. It monitors the input condition IN and sets the output Q as True whenever IN remains enabled for longer than a period of some input length PT. If the input in has been enabled for some time t < PT, then the timer sets the output ET (i.e., elapsed time) with value t; otherwise, it sets ET with value PT.

SDS2 uses diverse sensors and technologies to cause a reactor trip if SDS1 were to fail.

The underscore (..._) is used for generated names that conflict with PVS keywords.

The FBD is formalized over a discrete time series of equally distributed samplings, i.e., ticks. The pre operator returns the previous time sample.

The approach was qualified by trial use, inspection and acceptance testing.

Function block diagram (FBD), structured text (ST), instruction list (IL), ladder diagram (LD) and sequential function chart (SFC).

Blech, J.O., Biha, S.O.: On formal reasoning on the semantics of PLC using Coq. CoRR abs/1301.3047 (2013)

Darvas, D., Majzik, I., Blanco Viñuela, E.: Formal Verification of Safety PLC Based Control Software, pp. 508–522. Springer, Cham (2016)

DO-178C: Software Considerations in Airborne Systems and Equipment Certification. Special Committee 205 of RTCA (2011)

IEC: 61131-3 Ed. 3.0 en:2013: Programmable Controllers—Part 3: Programming Languages. International Electrotechnical Commission (2013)

IEEE 7-4.3.2: Standard for Digital Computers in Safety Systems of Nuclear Power Generating Stations (Revision of IEEE Std 7-4.3.2-2003). The Institute of Electrical and Electronics Engineers (IEEE) (2010)

Jimenez-Fraustro, F., Rutten, E.: A synchronous model of IEC 61131 PLC languages in SIGNAL. In: Euromicro Conference On Real-Time Systems, pp. 135–142 (2001)

Jin, Y., Parnas, D.L.: Defining the meaning of tabular mathematical expressions. Sci. Comput. Program. 75(11), 980–1000 (2010)CrossRefMATH

Joannou, P., Harauz, J., Viola, M., Cirjanic, R., Chan, D., Whittall, R., Tremaine, D., Moum, G.: Standard for Software Engineering of Safety Critical Software Revised for Application Oriented Language. CANDU Computer Systems Engineering Centre of Excellence Standard CE-1001-STD Rev. 3 (2014)

Nellen, J., Driessen, K., Neuhäußer, M., Ábrahám, E., Wolters, B.: Two CEGAR-based approaches for the safety verification of PLC-controlled plants. Inf. Syst. Front. 18(5), 927–952 (2016)CrossRef

10.

Németh, E., Bartha, T.: Formal verification of safety functions by reinterpretation of functional block based specifications. In: Formal Methods for Industrial Critical Systems. Springer, pp. 199–214 (2009)

11.

Newell, J., Pang, L., Tremaine, D., Wassyng, A., Lawford, M.: Formal translation of IEC 61131-3 function block diagrams to PVS with nuclear application. In: NASA Formal Methods—8th International Symposium, NFM 2016, Minneapolis, MN, USA, June 7–9, 2016, Proceedings. pp. 206–220 (2016)

12.

Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: International Conference on Automated Deduction. LNCS, vol. 607, pp. 748–752 (1992)

13.

Pang, L.: An Engineering Methodology for the Formal Verification of Function Block Based Systems. Ph.D. thesis, McMaster University, Department of Computing and Software (2015)

14.

Pang, L., Wang, C., Lawford, M., Wassyng, A.: Formal verification of function blocks applied to IEC 61131-3. Sci. Comput. Program. 113, 149–190 (2015)CrossRef

15.

Pang, L., Wang, C., Lawford, M., Wassyng, A., Newell, J., Chow, V., Tremaine, D.: Formal verification of real-time function blocks using PVS. In: Proceedings 4th International Workshop on Engineering Safety and Security Systems, ESSS 2015, Oslo, Norway, June 22, 2015, pp. 65–79 (2015)

16.

Parnas, D.L., Madey, J.: Functional documents for computer systems. Sci. Comput. Program. 25(1), 41–61 (1995)CrossRef

17.

Parnas, D.L., Madey, J., Iglewski, M.: Precise documentation of well-structured programs. IEEE Trans. Softw. Eng. 20, 948–976 (1994)CrossRef

18.

Soliman, D., Thramboulidis, K., Frey, G.: Transformation of function block diagrams to Uppaal timed automata for the verification of safety applications. Annu. Rev. Control. 36, 338–345 (2012)CrossRef

19.

Völker, N., Krämer, B.J.: Automated verification of function block-based industrial control systems. Sci. Comput. Program. 42(1), 101–113 (2002)CrossRefMATH

20.

Wassyng, A., Janicki, R.: Tabular expressions in software engineering. In: International Conference on Software & System Engineering and their Applications, vol. 4, pp. 1–46 (2003)

21.

Wassyng, A., Lawford, M.: Lessons learned from a successful implementation of formal methods in an industrial project. In: FME 2003: Formal Methods, LNCS, vol. 2805, pp. 133–153. Springer, Berlin, Heidelberg (2003)

Titel: Translation of IEC 61131-3 Function Block Diagrams to PVS for Formal Verification with Real-Time Nuclear Application
verfasst von: Josh Newell
Linna Pang
David Tremaine
Alan Wassyng
Mark Lawford
Publikationsdatum: 30.05.2017
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 1/2018
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-017-9415-7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 1/2018

Formal Verification of an Executable LTL Model Checker with Partial Order Reduction

Selected Extended Papers of NFM 2016: Preface

Synthesis of Obfuscation Policies to Ensure Privacy and Utility

Verifying Relative Safety, Accuracy, and Termination for Program Approximations

Safe Autonomy Under Perception Uncertainty Using Chance-Constrained Temporal Logic

Towards Probabilistic Formal Analysis of SATS-Simultaneously Moving Aircraft (SATS-SMA)