User Documentation

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].

References

results matching ""

    No results matching ""