A Methodological Guide for the Validation of Logic Modelling of Ladder Instructions
Un guide méthodologique pour la validation de modèles logiques des instructions Ladder
Résumé
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.
Les automates programmables industriels (PLC en anglais) sont des
dispositifs numériques industriels utilisés pour contrôler les processus de
fabrication automatisés, tels que les lignes d'assemblage. Le langage Ladder
est un langage de programmation utilisé pour développer des logiciels pour de
tels dispositifs. Dans un travail précédent, nous avons
proposé une méthode pour vérifier qu'un programme Ladder donné est conforme à
un comportement attendu exprimé par un diagramme de temps, décrivant un
scénario d'exécution. Cette méthode s'appuie sur une modélisation des
programmes Ladder en WhyML, le langage de l'environnement Why3 pour la
vérification déductive des programmes. Cette méthode s'appuie sur une
modélisation des instructions individuelles Ladder, à laquelle il faut faire
confiance.
Ce rapport propose une méthodologie pour accroître la confiance dans la
modélisation WhyML des instructions Ladder. Notre approche repose sur une
comparaison des exécutions d'un programme Ladder avec une exécution par Why3
d'une simulation du programme traduit. Grâce à cette technique, nous avons pu
valider notre modélisation des instructions Ladder, et également découvrir et corriger un
bug subtil dans la modélisation d’une instruction particulière.
Origine : Fichiers produits par l'(les) auteur(s)
licence : CC BY SA - Paternité - Partage selon les Conditions Initiales
licence : CC BY SA - Paternité - Partage selon les Conditions Initiales
