Transformation of non-standard nuclear I&C logic drawings to formal verification models
- Resource Type
- Conference
- Authors
- Pakonen, Antti; Biswas, Prasun; Papakonstantinou, Nikolaos
- Source
- IECON 2020 The 46th Annual Conference of the IEEE Industrial Electronics Society Industrial Electronics Society (IECON), 2020 The 46th Annual Conference of the IEEE. :697-704 Oct, 2020
- Subject
- Communication, Networking and Broadcast Technologies
Components, Circuits, Devices and Systems
Computing and Processing
Engineering Profession
Power, Energy and Industry Applications
Robotics and Control Systems
Signal Processing and Analysis
Transportation
Unified modeling language
Tools
Model checking
IEC Standards
XML
Industries
Standards
I&C
function block diagram
nuclear energy
IEC61131
PLCOpen XML
Model-Based System Engineering
- Language
- ISSN
- 2577-1647
Model checking methods have been proven to be a valuable asset for identifying undesired behaviour of safety-critical Instrumentation and Control (I&C) logics. Their application in the nuclear domain has been very successful and has triggered significant interest from the safety community. Creating formal models from the diagrams found on paper or from digital formats without the needed semantics is one bottleneck that hinders the adoption of model checking due to costs in time and may introduce errors. This paper proposes a methodology for the creation of formal models from I&C diagrams drawn in generic modelling tools (lacking specific I&C semantics). The generic I&C logic diagram is transformed into an intermediate UML model that in turn can be transformed to other target formats like IEC 61131 PLCopen XML I&C software or NuSMV formal model code. This methodology is demonstrated with a typical example of a trip signal generator application logic. This application logic is drawn in MS Visio, it is transformed to an I&C model in UML with the needed properties for model checking, then to IEC 61131 PLCopen XML and to an input file for the NuSMV model checker.