Automated Deductive Verification for Ladder Programming
This addresses debugging challenges for Ladder programmers in industrial automation, but it is incremental as it applies existing verification methods to a specific domain.
The paper tackles the problem of debugging Ladder Logic programs for industrial PLCs, which is time-consuming and error-prone, by presenting a Why3-based tool prototype that automates deductive verification to provide an easy-to-use and robust debugging tool.
Ladder Logics is a programming language standardized in IEC 61131-3 and widely used for programming industrial Programmable Logic Controllers (PLC). A PLC program consists of inputs (whose values are given at runtime by factory sensors), outputs (whose values are given at runtime to factory actuators), and the logical expressions computing output values from input values. Due to the graphical form of Ladder programs, and the amount of inputs and outputs in typical industrial programs, debugging such programs is time-consuming and error-prone. We present, in this paper, a Why3-based tool prototype we have implemented for automating the use of deductive verification in order to provide an easy-to-use and robust debugging tool for Ladder programmers.