Automated Verification of Temporal Properties of Ladder Programs

Cláudio Lourenço (1) , Denis Cousineau (2) , Florian Faissole (2) , Claude Marché (3) , David Mentré (2) , Hiroaki Inoue (4)

1 LMF - Laboratoire Méthodes Formelles
2 Mitsubishi Electric [France]
3 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
4 Mitsubishi Electric Corporation

Programmable Logic Controllers (PLCs) are industrial digital computers used as automation controllers in manufacturing processes. The Ladder language is a programming language used to develop PLC software. Our aim is to prove that a given Ladder program conforms to an expected temporal behaviour given as a timing chart, describing scenarios of execution. We translate the Ladder code and the timing chart into a program for the Why3 environment, within which the verification proceeds by generating verification conditions, to be checked valid using automated theorem provers. The ultimate goal is twofold: first, by obtaining a complete proof, we can verify the conformance of the Ladder code with respect to the timing chart with a high degree of confidence. Second, when the proof is not fully completed, we obtain a counterexample, illustrating a possible execution scenario of the Ladder code which does not conform to the timing chart.

Mots clés: Ladder language for programming PLCs; Timing charts; Formal specification; Deductive verification; Why3 environment

Domaines: Logique en informatique [cs.LO]

Cláudio Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, et al.. Automated Verification of Temporal Properties of Ladder Programs. FMICS 2021 - Formal Methods for Industrial Critical Systems, Aug 2021, Paris, France. ⟨10.1007/978-3-030-85248-1_2⟩. ⟨hal-03281580⟩