Formal Translation of IEC 61131-3 Function Block Diagrams to PVS with Nuclear Application
| Autor: | David Tremaine, Josh Newell, Mark Lawford, Alan Wassyng, Linna Pang |
|---|---|
| Rok vydání: | 2016 |
| Předmět: |
business.industry
Programming language Computer science IEC 61131-3 Programmable logic controller Block diagram Software requirements specification 020207 software engineering 02 engineering and technology Application software computer.software_genre Abstract syntax Formal specification 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Software engineering business computer Formal verification computer.programming_language |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783319406473 NFM |
| DOI: | 10.1007/978-3-319-40648-0_16 |
| Popis: | The trip computers for the two reactor shutdown systems of the Ontario Power Generation OPG Darlington Nuclear Power Generating Station DNGS 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 SRS written using tabular expressions TEs. The PVS theorem proving tool is used in the 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|