HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Reports

Formal Analysis of Ladder Programs using Deductive Verification

Abstract : Programmable logic controllers (PLC) are industrial digital computers used as automation controllers of manufacturing processes, such as assembly lines or robotic devices. The Ladder language, also known as Ladder Logic, is a programming language used to develop PLC software. Because of their widespread usage in industry, verifying that Ladder programs conform to their expected behaviour is of critical importance. In this work, we consider the description of the expected behaviour under the form of a timing chart, describing scenarios of execution. Our approach consists in translating the Ladder code and the timing chart into a program for the Why3 environment dedicated to deductive program verification. The verification proceeds by generating formal verification conditions, which are mathematical statements to be proved valid using automated theorem provers. The ultimate goal is two-fold: 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 :
Reports
Complete list of metadata

https://hal.inria.fr/hal-03199464
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Thursday, April 15, 2021 - 4:17:52 PM
Last modification on : Thursday, February 3, 2022 - 11:17:22 AM
Long-term archiving on: : Friday, July 16, 2021 - 7:00:57 PM

File

RR-9402.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03199464, version 1

Citation

Cláudio Lourenço, Denis Cousineau, Florian Faissole, Claude Marché, David Mentré, et al.. Formal Analysis of Ladder Programs using Deductive Verification. [Research Report] RR-9402, Inria. 2021, pp.25. ⟨hal-03199464⟩

Share

Metrics

Record views

128

Files downloads

194