Automated Deductive Verification for Ladder Programming

Denis Cousineau
(Mitsubishi Electric R&D Centre Europe (MERCE) Rennes, France)
David Mentré
(Mitsubishi Electric R&D Centre Europe (MERCE) Rennes, France)
Hiroaki Inoue
(Mitsubishi Electric Corporation Amagasaki, Japan)

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.

In Rosemary Monahan, Virgile Prevosto and Jose Proença: Proceedings Fifth Workshop on Formal Integrated Development Environment (F-IDE 2019), Porto, Portugal, 7th October 2019, Electronic Proceedings in Theoretical Computer Science 310, pp. 7–12.
Published: 23rd December 2019.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: