Un guide méthodologique pour la validation de modèles logiques des instructions Ladder
Denis Cousineau, Hiroaki Inoue, Claude Marché, David Mentré · HAL (Le Centre pour la Communication Scientifique Directe) · 2024
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 a previous work, we proposed a method for verifying that a given Ladder program conforms to an expected behaviour expressed by a timing chart, describing a scenario of execution. This method relies on a modelling of Ladder programs in WhyML, the language of the Why3 environment for deductive program verification. In this approach, the WhyML modelling of individual Ladder instructions has to be trusted.This report proposes a methodology to increase the trust in the WhyML modelling of Ladder instructions. Our approach relies on a comparison of the execution of Ladder programs with an execution by Why3 of a simulation of the translated program. With this technique, we have been able to validate our modelling of Ladder instructions, and also discover and fix a subtle bug in the modelling of one particular instruction.