We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Automated formal analysis of temporal properties of Ladder programs.
- Authors
Belo Lourenço, Cláudio; Cousineau, Denis; Faissole, Florian; Marché, Claude; Mentré, David; Inoue, Hiroaki
- Abstract
Programmable Logic Controllers are industrial digital computers used as automation controllers in manufacturing processes. The Ladder language is a programming language used to develop software for such controllers. In this work, we consider the description of the expected behaviour of a Ladder program under the form of a timing chart, describing a scenario of execution. Our aim is to prove that the given Ladder program conforms to the expected temporal behaviour given by such a timing chart. Our approach amounts to translating the Ladder code, together with the timing chart, into a program for the Why3 environment for deductive program verification. The verification proceeds with the generation of verification conditions: mathematical formulas to be checked valid using automated theorem provers. The ultimate goal is twofold. On the one hand, by obtaining a complete proof, one verifies the conformity of the Ladder code with respect to the timing chart with a high degree of confidence. On the other hand, in the case the proof is not fully completed, one obtains a counterexample, illustrating a possible execution scenario of the Ladder code which does not conform to the timing chart.
- Subjects
PROGRAMMABLE controllers; MANUFACTURING process automation; PROGRAMMING languages; MATHEMATICAL formulas
- Publication
International Journal on Software Tools for Technology Transfer, 2022, Vol 24, Issue 6, p977
- ISSN
1433-2779
- Publication type
Article
- DOI
10.1007/s10009-022-00680-0