Skip to Main content Skip to Navigation
Conference papers

Automated Verification of Temporal Properties of Ladder Programs

Abstract : 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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03281580
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Thursday, July 8, 2021 - 12:45:35 PM
Last modification on : Sunday, June 26, 2022 - 3:10:48 AM
Long-term archiving on: : Saturday, October 9, 2021 - 6:37:42 PM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

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⟩

Share

Metrics

Record views

83

Files downloads

123