Vérification de propriétés de sûreté dans les programmes Ladder Diagram

International audienceProgrammable Logical Controllers ensure the control of many reactive systems. Their programming is done with languages defined in the IEC 61131-3 standard. Our goal is the validation of safety properties of programs written in one of these languages: the Ladder Diagram. The main approaches in the field deal with Model-Checking. For our part, we propose to explore the way of the Theorem-Proving by defining a formal framework to express and handle the Ladder Diagram programs in a specific purpose algebra. Firstly, we define laws taking into account the specific statements of the language, then we prove some general theorems, and lastly, we present on an example an analysis leading to validation of safety properties.Les automates programmables industriels assurent le contrôle-commande d'un grand nombre de systèmes réactifs. Leur programmation se fait le plus souvent avec des langages définis dans la norme IEC 61131-3. Notre objectif est la validation de propriétés de sûreté dans les programmes écrits dans l'un de ces langages : le Ladder Diagram. Les principales approches dans le domaine abordent le problème par "Model-Checking". Pour notre part, nous nous proposons d'explorer la voie du "Theorem-Proving" en définissant un cadre formel pour exprimer et manipuler les programmes Ladder Diagram dans une algèbre adaptée. Après avoir défini des lois prenant en compte les primitives spécifiques du langage, puis après avoir démontré quelques théorèmes généraux, nous présentons sur un exemple une analyse conduisant à la validation de propriétés de sûreté