A toolset for model checking of PLC software
- 1 September 2013
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE) in 2013 IEEE 18th Conference on Emerging Technologies & Factory Automation (ETFA)
Abstract
Model checking is a powerful formal verification method that can also be used to evaluate PLC software. A lot of manual work and some expertise are still needed. Proposed methods for automating the process rely on standardised specification languages, but PLC software is often vendor-specific, and the source code for function blocks may not even be available. We propose a toolset for model checking of function block based software. After manually modelling the elementary function block library, the model of any block diagram can be specified with easy-to-use graphical tools. The counterexamples output by the model checker can also be visualised using a “living” function block diagram. Our toolset is based on integrating the popular model checker NuSMV with the open source modelling platform Simantics.Keywords
This publication has 7 references indexed in Scilit:
- Transformation of Function Block Diagrams to UPPAAL timed automata for the verification of safety applicationsAnnual Reviews in Control, 2012
- Model checking of safety-critical software in the nuclear engineering domainReliability Engineering & System Safety, 2012
- OPEN ONTOLOGY-BASED INTEGRATION PLATFORM FOR MODELING AND SIMULATION IN ENGINEERINGInternational Journal of Modeling, Simulation, and Scientific Computing, 2012
- VERIFICATION OF PLC PROGRAMS WRITTEN IN FBD WITH VISNuclear Engineering and Technology, 2009
- Efficient Representation for Formal Verification of PLC ProgramsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2006
- Minimal Assignments for Bounded Model CheckingLecture Notes in Computer Science, 2004
- Symbolic model checking: 1020 States and beyondInformation and Computation, 1992