ACCUEIL

Consignes aux
auteurs et coordonnateurs
Nos règles d'éthique
Auteurs : soumettez
votre article en ligne

APPEL À
CONTRIBUTION

Le comité de rédaction du JESA lance un appel à proposition de numéros spéciaux.

En savoir plus >>
Autres revues >>

Journal Européen des Systèmes Automatisés

1269-6935
Revues des Systèmes
 

 ARTICLE VOL 36/7 - 2002  - pp.905-917
TITLE
Safety Properties Verification of Ladder Diagram Programs

RÉSUMÉ
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 vérification 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 traduit les primitives de ce langage dans cette algèbre et donné des théorèmes généraux, nous présentons sur un exemple une analyse conduisant à la vérification de propriétés de sûreté.


ABSTRACT
Programmable Logic Controllers ensure the control of many reactive systems. These controllers are most of the time programmed with the languages defined in the IEC 61131­ 3 standard. Our goal is the verification of safety properties of programs written in one of these languages: the Ladder Diagram. The main approaches in this field are based on ModelChecking. We propose in this article a Theorem-Proving method by defining a formal framework to express and handle the Ladder Diagram programs with a specific algebra. Firstly, we translate the specific statements of the language into this algebra and we give some general theorems. Then, we present on an example an analysis leading to the verification of safety properties.


AUTEUR(S)
Jean-Marc ROUSSEL, Bruno DENIS

MOTS-CLÉS
Preuve de propriétés, Algèbre de Boole, Sûreté de Fonctionnement, Automates Programmables Industriels.

KEYWORDS
Properties Proof, Boolean Algebra, Safety, Programmable Logical Controllers.

LANGUE DE L'ARTICLE
Anglais

 PRIX
• Abonné (hors accès direct) : 7.5 €
• Non abonné : 15.0 €
|
|
--> Tous les articles sont dans un format PDF protégé par tatouage 
   
ACCÉDER A L'ARTICLE COMPLET  (99 Ko)



Mot de passe oublié ?

ABONNEZ-VOUS !

CONTACTS
Comité de
rédaction
Conditions
générales de vente

 English version >> 
Lavoisier