PLCverif

PLCverif is a tool developed at CERN to support formal verification of PLC programs. It translates the given PLC code and the specified requirement automatically to the input format of various model checker engines, and reports the result to the user in a readable format. Essentially it does model checking without needing any formal verification knowledge from the user.

Link to all related publications

Technical brief description.

Main features

Editor for SCL programs with syntax highlighting, content assist, and reference handling
Verification cases can be defined – these are the requirements to be checked
- The requirements can be given using requirement patterns
- Requirements are translated to temporal logic expressions in the background (needs no formal verification knowledge from the user)
Automated model generation from the given SCL code (STL, SFC are also partially supported)
Click-button verification: all steps are hidden and automatised – the user just imports/edits the code, defines the verification case and hits the "Verify" button
- The translation process contains various automated model reductions
Verification report gives feedback to the user about the checked verification case, including the counterexample, if it exists.
Besides the graphical interface, the tool has a command line interface. This allows to automate verification using scripts or continuous integration tools (e.g. Jenkins).


1 - SCL editor	2 - Requirement pattern	3 - Verification case	4 - Verification report	5 - Integration with Jenkins

Applied technologies

Eclipse RCP (Mars)
Eclipse Modeling Framework
Xtext (2.9)
Xtend (2.9)
Zest (1.5)
GraphViz (2.36)

Underlying model checker engines

Full integration with
- NuSMV (2.5.4+) and nuXmv (1.0.1+)
- CBMC (5.8)
- Theta
Model generation also supported for UPPAAL, BIP, PetriDotNet, TTMC and ITS tools (GAL)

Distribution

Since August 2020, the tool (source code and executable) is released as an open source project under the EPL 2.0 License (Eclipse Public License - v 2.0).

The source code is available on GitLab.

The latest releases for Windows and Linux are available here. Previous releases are available at the bottom of this page.

Make sure to read the user and developer documentation first.

Finally, remember that PLCverif needs at least one of the three supported model checkers which have to be installed independently.

More information & links

For more information, contact us or read our toolpaper: D. Darvas, B. Fernández Adiego, E. Blanco Viñuela. PLCverif: A tool to verify PLC programs based on model checking techniques. In Proc. of the 15th International Conference on Accelerator and Large Experimental Physics Control Systems, p. 911-915. [Paper]