PLCverif is an advanced tool developed at CERN to support the formal verification of PLC (Programmable Logic Controller) programs. It takes PLC program code and verifies it against a set of provided requirements, producing results that are understandable to the automation engineers. Essentially, PLCverif performs model checking with mathematical soundness, but without needing any deep formal verification knowledge from the user.
The tool translates PLC code and the specified requirements automatically to the input format of various model checker engines, and reports the result to the user in a convenient, easy-to-understand format. PLCverif is a customizable and extensible, plugin-based framework that can be extended to support the verification of programs written in various programming languages, also to support different types of requirements and external verification engines.
The PLCverif tool relies on external formal verification tools. The tool, as well as the methodology behind is general, thus it can be applied to various programs, requirements and verification tools. To be able to exploit this in practice, PLCverif can be extended by plug-ins. Each plug-in adapts a PLC programming language, a verification tool, model reductions or a reporting mechanism.
This document provides a short overview of the usage and extensibility of the tool. It focuses on the knowledge that is essential for a user. Information about the internal mechanisms and about the whole workflow can be found in previous CERN Internal Notes [1, 3] and papers [2, 4, 5].
-  D. Darvas et al. Transforming PLC programs into formal models for verification purposes. Internal Note CERN-ACC-NOTE-2013-0040, CERN, 2013.
-  D. Darvas et al. Formal verification of complex properties on PLC programs. FORTE 2014, LNCS 8461. 2014.
-  B. Fernández et al. Automated generation of formal models from ST control programs for verification purposes. Internal Note CERN-ACC-NOTE-2014-0037, CERN, 2014.
-  B. Fernández et al. Bringing automated model checking to PLC program development -- A CERN case study. WODES 2014.
-  B. Fernández et al. Applying model checking to industrial-sized PLC programs. IEEE Transactions on Industrial Informatics, 11(6):1400-1410, 2015.