💬 NLP

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

Dit artikel introduceert ESBMC-GraphPLC, een formeel verificatie-instrument dat de kloof in de verwerking van grafische PLCopen XML Ladder Diagrammen overbrugt door een op DFS gebaseerde resolver te implementeren om grafische rung-logica om te zetten naar een geldige GOTO intermediaire representatie voor SMT-gebaseerde model checking, waardoor een correcte verificatie van programma's uit editors zoals CONTROLLINO en OpenPLC Editor mogelijk wordt zonder de bestaande ondersteuning voor tekstuele formaten aan te tasten.

Oorspronkelijke auteurs: Pierre Dantas, Lucas Cordeiro, Waldir Junior

Gepubliceerd 2026-06-19

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Pierre Dantas, Lucas Cordeiro, Waldir Junior

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je een Programmable Logic Controller (PLC) voor als het brein van een machine in een fabriek, zoals een waterpomp of een verkeerslicht. Om dit brein te vertellen wat het moet doen, tekenen ingenieurs Ladder Diagrammen. Deze zien eruit als elektrische ladders met sporten, waarbij elke sport een regel is: "Als de watertank vol is, zet de pomp uit."

Een lange tijd waren er twee manieren om deze laddertekeningen op een computer op te slaan:

De Tekstlijst: Een eenvoudige, stapsgewijze lijst met instructies (zoals een recept).
De Grafische Kaart: Een visuele kaart waar onderdelen door middel van onzichtbare draden met elkaar zijn verbonden, geïdentificeerd door ID-nummers (zoals een metrokaart waarbij stations door lijnen worden verbonden).

Het Probleem: Het "Geest"-programma

De onderzoekers hadden een krachtige tool genaamd ESBMC-PLC die deze programma's kon controleren op veiligheidsfouten. Het werkte perfect op het Tekstlijst-formaat.

Echter, wanneer ze het Grafische Kaart-formaat invoerden (wat moderne software zoals CONTROLLINO en OpenPLC daadwerkelijk gebruikt), raakte de tool in de war. De tool keek naar de kaart, zag de ID-nummers en draden, maar begreep niet hoe deze met elkaar verbonden waren.

Het resultaat: De tool zei: "Alles is veilig!"
De adder onder het gras: Het was een leugen. Het was niet veilig omdat de logica ontbrak; het was "veilig" omdat de tool naar een lege kamer keek. Dit wordt vacuous verification (leegstaande verificatie) genoemd — het is alsof je zegt dat een vergrendelde deur beveiligd is omdat je bent vergeten te controleren of er een raam openstaat.

De Oplossing: ESBMC-GraphPLC

De auteurs bouwden een nieuwe module genaamd ESBMC-GraphPLC om dit op te lossen. Denk aan het inhuren van een detective die door de grafische kaart loopt en deze terugvertaalt naar een taal die de veiligheidscontrole begrijpt.

Hier is hoe hun "detective" werkt, met behulp van eenvoudige analogieën:

1. De Detective met een Zaklamp (DFS Algoritme)
De tool gebruikt een methode genaamd Depth-First Search (DFS). Stel je een detective voor die door een doolhof van draden loopt. Ze beginnen aan de linkerkant van de ladder (de stroombron) en volgen elk mogelijk pad naar de rechterkant.

Ze traceren elke draadverbinding.
Ze schrijven elke schakelaar (contact) op die ze passeren.
Ze stoppen wanneer ze het apparaat (de spoel/pomp) bereiken.
Door dit te doen, reconstrueren ze de exacte logica van de ladder-sport en veranderen ze de visuele kaart terug in een duidelijke "Als-Dan" regel.

2. De Verkeersregelaar (Volgorde is belangrijk)
In deze diagrammen heb je soms een "Set"-schakelaar (aan zetten) en een "Reset"-schakelaar (uit zetten) voor hetzelfde apparaat. De volgorde is cruciaf!

Als de "Reset" plaatsvindt na de "Set" in precies hetzelfde fractie van een seconde, blijft het apparaat uit.
Als de "Set" plaatsvindt na de "Reset", blijft het apparaat aan.
De nieuwe tool kijelt naar een specifieke lijst in het bestand (de rightPowerRail sequentie) om te zien welke schakelaar eerst komt, optredend als een verkeersregelaar die ervoor zorgt dat de "Set"-auto vóór de "Reset"-auto gaat. Dit zorgt ervoor dat de logica overeenkomt met hoe echte machines zich daadwerkelijk gedragen.

3. Het Raadspelletje (I/O Inferentie)
Soms zegt de kaart niet welke draden "Inputs" (sensoren) en welke "Outputs" (motoren) zijn. De tool gebruikt een driestappen-raadspel:

Stap 1: Zoek naar officiële adreslabels (zoals %IX voor inputs). Als deze gevonden worden, is het exact.
Stap 2: Als er geen labels zijn, kijk dan naar het gedrag. Als een draad alleen als schakelaar wordt gebruikt, is het waarschijnlijk een input. Als het alleen wordt gebruikt om iets aan te zetten, is het waarschijnlijk een output.
Stap 3: Als er nog steeds onduidelijkheid is, behandel het dan als een "mysterieus variabele" die alles kan zijn. Dit is een veilige keuze, omdat het alle mogelijkheden controleert, zodat er niets gemist wordt.

De Resultaten

Het team heeft deze nieuwe detective getest op drie real-world programma's (waterpompen, trapleuken en dimbare lichten).

Vóór: De tool zag een lege kamer en zei "Veilig" (onjuist).
Nadat: De tool zag de volledige logica, controleerde elke mogelijke combinatie van sensor-inputs en bevestigde dat de programma's daadwerkelijk veilig waren.
Snelheid: Dit deed het in minder dan 70 milliseconden (sneller dan een menselijke knipoog).
Veiligheid: Het heeft de oude tool niet kapot gemaakt. De 11 programma's die al werkten met tekstlijsten, werkten nog steeds perfect.

Wat het nog niet kan (De Beperkingen)

Het paper is eerlijk over waar de detective nog mee worstelt:

Complexe Timers: Als een sport een timer bevat (bijv. "Wacht 5 seconden, zet dan aan"), negeert de tool momenteel het "wacht"-gedeelte en behandelt het als een willekeurige gok. Het is veilig, maar het begrijpt de timing niet.
Geneste Kaarten: Sommige complexe diagrammen verbergen kleinere kaarten binnen andere secties (zoals acties binnen een stap). De detective mist deze verborgen kamers soms.

Samenvatting

Kortom, de auteurs hebben een vertaler gebouwd die ervoor zorgt dat veiligheidscontrole-software eindelijk de visuele ladderdiagrammen kan "lezen" die door moderne industriële software worden gebruikt. Ze hebben een tool die blindelings "Alles is in orde" riep, veranderd in een tool die de logica daadwerkelijk begrijpt en kan bewijzen dat de machine niet zal breken of mensen zal verwonden.

Technische Samenvatting: ESBMC-GraphPLC

Probleemstelling
Het artikel adresseert een kritieke tekortkoming in de formele verificatie van PLC-programma's (Programmable Logic Controller) met behulp van de ESBMC-PLC tool. Hoewel ESBMC-PLC het tekstuele formaat van PLCopen XML (tc6_0201) succesvol ondersteunde, slaagde het er niet in om het grafische formaat correct te verwerken, wat het natuurlijke exportformaat is voor belangrijke ontwikkelomgevingen zoals CONTROLLINO, Beremiz en OpenPLC Editor.

In het grafische formaat wordt de Ladder Diagram (LD) logica gecodeerd als een gerichte graaf van localId en refLocalId verbindingen in plaats van expliciete <rung> elementen. De bestaande parser detecteerde deze bestanden wel, maar vond geen rungs, wat resulteerde in een lege GOTO Intermediate Representation (IR). Bijgevolg bleven alle variabelen geïnitialiseerd op nul, waardoor de verificatie vacuüm slaagde: eigenschappen werden triviaal voldaan omdat er geen logica werd gegenereerd. Dit bood geen werkelijke garantie met betrekking tot de veiligheid van de PLC-logica.

Methodologie
De auteurs introduceren ESBMC-GraphPLC, een module die dit gat overbrugt door een op Depth-First Search (DFS) gebaseerde resolver te implementeren om de rung-logica te reconstrueren uit de grafische verbindingsgraaf. De methodologie bestaat uit drie kerncomponenten:

Grafische LD Resolver & Rung Extractie:
- Het systeem parseert de localId/refLocalId graaf om paden van de leftPowerRail naar elke coil te identificeren.
- Het doorloopt de graaf om sequenties van contacten te extraheren en converteert deze naar Booleaanse conjuncties.
- Cruciaal Inzicht in Ordening: Om te voldoen aan de IEC 61131-3 scan-cycle semantiek, ordent het algoritme de verwerking van coils op basis van de volgorde van de refLocalId entries in de rightPowerRail's connectionPointIn lijst. Dit zorgt ervoor dat SET coils vóór RESET coils worden verwerkt binnen dezelfde scan-cycle, waardoor de correcte latch-werking behouden blijft.
Drie-lagen I/O Inferentie:
Om inputs (nondeterministische her-sampling) en outputs (persistente staat) correct te modelleren, hanteert de tool een gelaagd classificatieschema:
- Laag 1: Gebruikt expliciete IEC 61131-3 hardwareadressen (%IX voor inputs, %QX voor outputs).
- Laag 2: Past een heuristische analyse toe voor adresseloze programma's, waarbij variabelen die alleen als contacten voorkomen als inputs worden geclassificeerd en variabelen die alleen als coils voorkomen als outputs.
- Laag 3: Behandelt ongeclassificeerde variabelen als interne persistente staat.
Implementatiestrategie:
De oplossing is volledig geïmplementeerd binnen de frontend parser (plcopen_xml_parser.cpp, +274 regels). Het vereist geen enkele wijziging in de ESBMC backend, inclusief de GOTO IR encoder, k-induction engine, Z3 SMT solver of property encoder. De resolver genereert een standaard RungNode lijst, identiek aan de structuur geproduceerd door de tekstuele parser.

Belangrijkste Bijdragen

Formeel Model: Een formele definitie van de grafische LD verbindingsgraaf en een bewijs van de soundness die aantoont dat de via DFS geëxtraheerde paden equivalent zijn aan de IEC 61131-3 scan-cycle semantiek.
Algoritmische Oplossing: De eerste open-source implementatie van een DFS-gebaseerde rung extractor voor grafische PLCopen XML die de SET/RESET ordening correct afhandelt.
Compatibiliteit achterwaarts: De extensie behoudt alle bestaande functionaliteit voor tekstuele LD benchmarks met nul regressies.
Artefact: Een compleet, reproduceerbaar artefact inclusief de tool, benchmarks en een Python-prototype voor validatie.

Experimentele Resultaten
De tool werd geëvalueerd op 3 grafische LD programma's geëxporteerd uit CONTROLLINO en OpenPLC Editor:

Water Control (water_control): 5 rungs (2 SET, 3 RESET).
Staircase Light (stairs_light): 6 rungs (2 SET, 2 RESET, 2 plain).
Dimmer Light (dimmer_light_control): 4 rungs (plain).

Resultaten:

IR Volledigheid: Alle 3 programma's gingen over van een "Empty IR" (vacuüm) naar een "Full IR" bevattende nondeterministische inputs en volledige rung-logica.
Verificatie: Alle 3 programma's werden geverifieerd als SAFE bij $k=2$ in minder dan 70 ms (mediane tijden: 50ms, 40ms, 60ms).
Regressie: De 11 authentieke tekstuele LD benchmarks van ESBMC-PLC produceerden identieke resultaten, wat bevestigt dat er geen sprake is van regressies.

Beperkingen en Reikwijdte
Het artikel merkt expliciet op dat de huidige resolver de semantiek van function blocks (timers, counters, comparators) binnen rung-paden niet behoudt. Als een rung afhankelijk is van een function block, behandelt de tool de output van het blok als een nondeterministische term (sound over-approximation) of, in specifieke gevallen zoals het beremiz_traffic_light voorbeeld, stort de logica in tot een constante. Twee Beremiz voorbeelden werden uitgesloten van de hoofdresultaten om te voorkomen dat er misleidende "SAFE" verdicts worden gerapporteerd voor programma's waar de timing-semantiek verloren is gegaan.

Betekenis
Het artikel stelt dat ESBMC-GraphPLC de sound, non-vacuous formele verificatie mogelijk maakt van grafische PLCopen XML programma's, die de standaardoutput zijn van moderne PLC-ontwikkelomgevingen. Door de kloof tussen grafische exports en SMT-gebaseerde model checking te dichten, stelt de tool automatiseringstechnici in staat om veiligheidseigenschappen (bijv. pompcontrole, verkeerslichten) te verifiëren zonder handmatige conversie naar tekstuele formaten. De auteurs benadrukken dat hoewel de huidige implementatie contact/coil netwerken met SET/RESET latches effectief afhandelt, toekomstig werk vereist is om de function-block semantiek te integreren voor het ondersteunen van complexere sequentiële controlelogica.