💬 NLP

ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking

Cet article présente ESBMC-GraphPLC, un outil de vérification formelle qui comble la lacune dans la gestion des diagrammes à échelons (Ladder Diagrams) au format XML PLCopen en implémentant un résolveur basé sur une recherche en profondeur (DFS) pour convertir la logique de barreaux sous forme de graphe en une représentation intermédiaire GOTO valide pour la vérification de modèles basée sur le SMT, permettant ainsi la vérification correcte de programmes provenant d'éditeurs tels que CONTROLLINO et OpenPLC Editor sans affecter le support existant du format textuel.

Auteurs originaux : Pierre Dantas, Lucas Cordeiro, Waldir Junior

Publié 2026-06-19

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Pierre Dantas, Lucas Cordeiro, Waldir Junior

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez un Automate Programmable Industriel (API) comme le cerveau d'une machine d'usine, comme une pompe à eau ou un feu de signalisation. Pour dire à ce cerveau quoi faire, les ingénieurs dessinent des Diagrammes en échelle. Ils ressemblent à des échelles électriques avec des échelons, où chaque échelon est une règle : « Si le réservoir d'eau est plein, éteignez la pompe. »

Pendant longtemps, il y avait deux façons d'enregistrer ces dessins en échelle sur un ordinateur :

La Liste de Texte : Une liste simple et étape par étape d'instructions (comme une recette).
La Carte Graphique : Une carte visuelle où des pièces sont connectées par des fils invisibles, identifiées par des numéros d'ID (comme une carte de métro où les stations sont reliées par des lignes).

Le Problème : Le Programme « Fantôme »

Les chercheurs possédaient un outil puissant appelé ESBMC-PLC qui pouvait vérifier la sécurité de ces programmes. Il fonctionnait parfaitement sur le format de la Liste de Texte.

Cependant, lorsqu'ils ont soumis le format de la Carte Graphique (qui est ce que les logiciels modernes comme CONTROLLINO et OpenPLC utilisent réellement), l'outil a été confus. Il regardait la carte, voyait les numéros d'ID et les fils, mais ne comprenait pas comment ils se connectaient.

Le Résultat : L'outil disait : « Tout est sûr ! »
Le Piège : Il mentait. Ce n'était pas sûr parce que la logique était absente ; c'était « sûr » parce que l'outil regardait une pièce vide. C'est ce qu'on appelle la vérification vacante — c'est comme dire qu'une porte verrouillée est sécurisée parce que vous avez oublié de vérifier si une fenêtre est ouverte.

La Solution : ESBMC-GraphPLC

Les auteurs ont construit un nouveau module appelé ESBMC-GraphPLC pour corriger cela. Considérez cela comme l'embauche d'un détective pour parcourir la carte graphique et la traduire dans un langage que le vérificateur de sécurité peut comprendre.

Voici comment leur « détectif » fonctionne, en utilisant des analogies simples :

1. Le Détective avec une Lampe de Poche (Algorithme DFS)
L'outil utilise une méthode appelée Recherche en Profondeur (DFS - Depth-First Search). Imaginez un détective parcourant un labyrinthe de fils. Il commence du côté gauche de l'échelle (la source d'alimentation) et suit chaque chemin possible vers le côté droit.

Il trace chaque connexion de fil.
Il note chaque interrupteur (contact) qu'il rencontre.
Il s'arrête lorsqu'il atteint le dispositif (la bobine/pompe).
Ce faisant, il reconstruit la logique exacte de l'échelon de l'échelle, transformant la carte visuelle en une règle claire de type « Si-Alors ».

2. Le Agent de Circulation (L'ordre compte)
Dans ces diagrammes, vous avez parfois un interrupteur « Set » (allumer) et un interrupque « Reset » (éteindre) pour le même dispositif. L'ordre est important !

Si le « Reset » se produit après le « Set » dans la même fraction de seconde, le dispositif reste éteint.
Si le « Set » se produit après le « Reset », le dispositif reste allumé.
Le nouvel outil examine une liste spécifique dans le fichier (la séquence rightPowerRail) pour voir quel interrupteur vient en premier, agissant comme un agent de circulation s'assurant que la voiture « Set » passe avant la voiture « Reset ». Cela garantit que la logique correspond au comportement réel des machines.

3. Le Jeu de Devinettes (Inférence d'E/S)
Parfois, la carte ne précise pas quels fils sont des « Entrées » (capteurs) et lesquels sont des « Sorties » (moteurs). L'outil utilise un jeu de devinettes en trois étapes :

Étape 1 : Chercher des étiquettes d'adresses officielles (comme %IX pour les entrées). Si elles sont trouvées, c'est précis.
Étape 2 : Si aucune étiquette n'est présente, observer le comportement. Si un fil est uniquement utilisé comme interrupteur, c'est probablement une entrée. S'il est uniquement utilisé pour allumer quelque chose, c'est probablement une sortie.
Étape 3 : Si l'incertitude persiste, traiter le fil comme une « variable mystère » qui pourrait être n'importe quoi. C'est un pari sûr car cela vérifie toutes les possibilités, garantissant que rien n'est oublié.

Les Résultats

L'équipe a testé ce nouveau détective sur trois programmes réels (pompes à eau, lumières d'escalier et variateurs de lumière).

Avant : L'outil voyait une pièce vide et disait « Sûr » (incorrectement).
Après : L'outil a vu toute la logique, a vérifié toutes les combinaisons possibles d'entrées de capteurs et a confirmé que les programmes étaient réellement sûrs.
Vitesse : Il a fait cela en moins de 70 millisecondes (plus vite qu'un clin d'œil humain).
Sécurité : Il n'a pas cassé l'ancien outil. Les 11 programmes qui fonctionnaient déjà avec les listes de texte fonctionnaient toujours parfaitement.

Ce qu'il ne peut pas encore faire (Les Limites)

L'article est honnête sur les difficultés persistantes du détective :

Temporisateurs Complexes : Si un échelon implique un temporisateur (ex: « Attendre 5 secondes, puis allumer »), l'outil ignore actuellement la partie « attente » et la traite comme une supposition aléatoire. C'est sûr, mais il ne comprend pas la gestion du temps.
Cartes Imbriquées : Certains diagrammes complexes cachent de plus petites cartes à l'intérieur d'autres sections (comme des actions à l'intérieur d'une étape). Le détective manque parfois ces pièces cachées.

Résumé

En résumé, les auteurs ont construit un traducteur qui permet aux logiciels de vérification de sécurité de enfin « lire » les diagrammes en échelle visuels utilisés par les logiciels industriels modernes. Ils ont transformé un outil qui disait aveuglément « Tout va bien » en un outil qui comprend réellement la logique et peut prouver que la machine ne cassera pas ou ne blessera personne.

Résumé Technique : ESBMC-GraphPLC

Énoncé du Problème
Le document traite d'une lacune critique dans la vérification formelle des programmes d'Automates Programmables Industriels (API/PLC) utilisant l'outil ESBMC-PLC. Bien qu'ESBMC-PLC ait réussi à prendre en charge le format textuel de l'XML PLCopen (tc6_0201), il ne parvenait pas à traiter correctement le format graphique, qui est le format d'exportation natif des environnements de développement majeurs tels que CONTROLLINO, Beremiz et OpenPLC Editor.

Dans le format graphique, la logique du diagramme à contacts (Ladder Diagram - LD) est encodée sous la forme d'un graphe orienté de connexions localId et refLocalId plutôt que par des éléments <rung> explicites. Le parseur existant détectait ces fichiers mais ne trouvait aucun échelon (rung), ce qui résultait en une représentation intermédiaire (IR) GOTO vide. Par conséquent, toutes les variables restaient initialisées à zéro, ce qui rendait la vérification réussie de manière vacueuse : les propriétés étaient trivialement respectées car aucune logique n'était générée. Cela ne fournissait aucune garantie réelle concernant la sécurité de la logique de l'API.

Méthodologie
Les auteurs introduisent ESBMC-GraphPLC, un module qui comble cette lacune en implémentant un résolveur basé sur une recherche en profondeur (DFS) pour reconstruire la logique des échelons à partir du graphe de connexion graphique. La méthodologie comprend trois composantes centrales :

Résolveur de LD Graphique & Extraction d'Échelons :
- Le système analyse le graphe localId/refLocalId pour identifier les chemins allant du rail d'alimentation gauche (leftPowerRail) vers chaque bobine (coil).
- Il parcourt le graphe pour extraire des séquences de contacts, les convertissant en conjonctions booléennes.
- Aperçu critique de l'ordonnancement : Pour respecter la sémantique du cycle de balayage (scan-cycle) de la norme IEC 61131-3, l'algorithme ordonne le traitement des bobines en fonction de la séquence des entrées refLocalId dans la liste connectionPointIn du rail d'alimentation droit (rightPowerRail). Cela garantit que les bobines SET sont traitées avant les bobines RESET au sein d'un même cycle de balayage, préservant ainsi le comportement de verrouillage (latch) correct.
Inférence d'E/S à trois niveaux :
Pour modéliser correctement les entrées (ré-échantillonnage non déterministe) et les sorties (état persistant), l'outil utilise un schéma de classification à trois niveaux :
- Niveau 1 : Utilise les adresses matérielles explicites de la norme IEC 61131-3 (%IX pour les entrées, %QX pour les sorties).
- Niveau 2 : Applique une analyse heuristique pour les programmes sans adresse, classant les variables apparaissant uniquement comme contacts comme entrées, et celles apparaissant uniquement comme bobines comme sorties.
- Niveau 3 : Traite les variables non classées comme un état interne persistant.
Stratégie d'Implémentation :
La solution est entièrement implémentée dans le parseur frontal (plcopen_xml_parser.cpp, +274 lignes). Elle ne nécessite aucun changement au backend d'ESBMC, y compris l'encodeur d'IR GOTO, le moteur de k-induction, le solveur SMT Z3 ou l'encodeur de propriétés. Le résolveur produit une liste de RungNode standard, identique à la structure produite par le parseur textuel.

Principales Contributions

Modèle Formel : Une définition formelle du graphe de connexion LD graphique et un théorème de correction prouvant que les chemins extraits par DFS sont équivalents aux sémantiques de cycle de balayage IEC 61131-3.
Solution Algorithmique : La première implémentation open-source d'un extracteur d'échelons par DFS pour le XML PLCopen graphique qui gère correctement l'ordonnancement SET/RESET.
Compatibilité Ascendante : L'extension préserve toutes les fonctionnalités existantes pour les benchmarks LD textuels avec zéro régression.
Artéfact : Un artéfact complet et reproductible incluant l'outil, les benchmarks et un prototype Python pour la validation.

Résultats Expérimentaux
L'outil a été évalué sur 3 programmes LD graphiques exportés de CONTROLLINO et OpenPLC Editor :

Contrôle de l'eau (water_control) : 5 échelons (2 SET, 3 RESET).
Éclairage d'escalier (stairs_light) : 6 échelons (2 SET, 2 RESET, 2 simples).
Contrôle de variateur (dimmer_light_control) : 4 échelons (simples).

Résultats :

Complétude de l'IR : Les 3 programmes sont passés d'une production d'une "IR Vide" (vacueuse) à une "IR Complète" contenant des entrées non déterministes et une logique d'échelon complète.
Vérification : Les 3 programmes ont été vérifiés comme SÛRS (SAFE) à $k=2$ en moins de 70 ms (temps médians : 50ms, 40ms, 60ms).
Régression : Les 11 benchmarks LD textuels authentiques d'ESBMC-PLC ont produit des résultats identiques, confirmant l'absence de régression.

Limites et Portée
Le papier note explicitement que le résolveur actuel ne préserve pas la sémantique des blocs fonctionnels (temporisateurs, compteurs, comparateurs) au sein des chemins d'échelons. Si un échelon dépend d'un bloc fonctionnel, l'outil traite la sortie du bloc comme un terme non déterministe (sur-approximation saine) ou, dans certains cas comme l'exemple beremiz_traffic_light, la logique s'effondre vers une constante. Deux exemples de Beremiz ont été exclus des résultats principaux pour éviter de rapporter des verdicts "SAFE" trompeurs pour des programmes où la sémantique temporelle était perdue.

Signification
Le papier affirme qu'ESBMC-GraphPLC permet la vérification formelle non vacueuse et saine des programmes PLCopen XML graphiques, qui sont le standard de sortie des environnements de développement d'API modernes. En comblant l'écart entre les exports graphiques et le model checking basé sur SMT, l'outil permet aux ingénieurs en automatisation de vérifier les propriétés de sécurité (ex: contrôle de pompe, feux de signalisation) sans conversion manuelle vers des formats textuels. Les auteurs soulignent que si l'implémentation actuelle gère efficacement les réseaux de contacts/bobines avec les verrouillages SET/RESET, des travaux futurs sont nécessaires pour intégrer la sémantique des blocs fonctionnels afin de supporter des logiques de contrôle séquentiel plus complexes.