💬 NLP

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

Questo articolo introduce ESBMC-GraphPLC, uno strumento di verifica formale che colma la lacuna nella gestione dei diagrammi a scala XML in formato PLCopen implementando un risolutore basato su DFS per convertire la logica dei rami basata su grafi in una rappresentazione intermedia GOTO valida per il model checking basato su SMT, abilitando così la corretta verifica di programmi provenienti da editor come CONTROLLINO e OpenPLC Editor senza influenzare il supporto esistente per i formati testuali.

Autori originali: Pierre Dantas, Lucas Cordeiro, Waldir Junior

Pubblicato 2026-06-19

📖 5 min di lettura🧠 Approfondimento

CC BY 4.0

Autori originali: Pierre Dantas, Lucas Cordeiro, Waldir Junior

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

Immagina un Controllore Logico Programmabile (PLC) come il cervello di una macchina di fabbrica, come una pompa dell'acqua o un semaforo. Per dire a questo cervello cosa fare, gli ingegneri disegnano i Diagrammi a Scala (Ladder Diagrams). Questi sembrano scale elettriche con i pioli, dove ogni piolo è una regola: "Se il serbatoio dell'acqua è pieno, spegni la pompa".

Per molto tempo, c'erano due modi per salvare questi disegni a scala su un computer:

L'Elenco Testuale: Un semplice elenco passo dopo passo di istruzioni (come una ricetta).
La Mappa Grafica: Una mappa visiva dove i pezzi sono collegati da fili invisibili, identificati da numeri di ID (come una mappa della metropolitana dove le stazioni sono collegate da linee).

Il Problema: Il Programma "Fantasma"

I ricercatori avevano uno strumento potente chiamato ESBMC-PLC che poteva controllare questi programmi per errori di sicurezza. Funzionava perfettamente sul formato dell'Elenco Testuale.

Tuttavia, quando fornivano il formato della Mappa Grafica (che è ciò che i software moderni come CONTROLLINO e OpenPLC utilizzano effettivamente), lo strumento si confondeva. Guardava la mappa, vedeva i numeri di ID e i fili, ma non riusciva a capire come si collegassero.

Poiché non riusciva a leggere la mappa, assumeva che non stesse succedendo nulla. Pensava che ogni interruttore fosse spento e ogni pompa ferma.
Il Risultato: Lo strumento diceva: "Tutto è sicuro!"
L'Imbroglio: Stava mentendo. Non era sicuro perché la logica era assente; era "sicuro" perché lo strumento stava guardando una stanza vuota. Questo è chiamato verifica vacua — è come dire che una porta chiusa è sicura perché ti sei dimenticato di controllare se c'è una finestra aperta.

La Soluzione: ESBMC-GraphPLC

Gli autori hanno costruito un nuovo modulo chiamato ESBMC-GraphPLC per risolvere il problema. Immagina di assumere un detective per camminare attraverso la mappa grafica e tradurla nuovamente in un linguaggio che il controllore di sicurezza possa comprendere.

Ecco come funziona il loro "detective", usando semplici analogie:

1. Il Detective con la Torcia (Algoritmo DFS)
Lo strumento utilizza un metodo chiamato Ricerca in Profondità (Depth-First Search - DFS). Immagina un detective che cammina attraverso un labirinto di fili. Inizia dal lato sinisto della scala (la sorgente di alimentazione) e segue ogni possibile percorso verso il lato destro.

Traccia ogni connessione dei fili.
Annota ogni interruttore (contatto) che incontra.
Si ferma quando raggiunge il dispositivo (la bobina/pompa).
Facendo questo, ricostruisce la logica esatta del piolo della scala, trasformando la mappa visiva di nuovo in una chiara regola "Se-Allora".

2. Il Vigile Urbano (L'ordine è importante)
In questi diagrammi, a volte hai un interruttore "Set" (accendi) e un interruttore "Reset" (spegni) per lo stesso dispositivo. L'ordine conta!

Se il "Reset" avviene dopo il "Set" nello stesso istante, il dispositivo rimane spento.
Se il "Set" avviene dopo il "Reset", il dispositivo rimane acceso.
Il nuovo strumento osserva una lista specifica nel file (la sequenza rightPoweringRail) per vedere quale interruttore viene prima, agendo come un vigile urbano che assicura che l'auto "Set" passi prima dell'auto "Reset". Ciò garantisce che la logica corrisponda al modo in cui le macchine reali si comportano effettivamente.

3. Il Gioco dell'Indovino (Inferenza I/O)
A volte la mappa non dice quali fili sono "Input" (sensori) e quali sono "Output" (motori). Lo strumento usa un gioco di indovinelli in tre fasi:

Fase 1: Cerca etichette di indirizzo ufficiali (come %IX per gli input). Se trovate, sono esatte.
Fase 2: Se non ci sono etichette, osserva il comportamento. Se un filo è usato solo come interruttore, è probabilmente un input. Se è usato solo per accendere qualcosa, è probabilmente un output.
Fase 3: Se non è ancora sicuro, lo tratta come una "variabile misteriosa" che potrebbe essere qualsiasi cosa. Questa è una scelta sicura perché controlla tutte le possibilità, assicurando che nulla venga tralasciato.

I Risultati

Il team ha testato questo nuovo detective su tre programmi del mondo reale (pompe dell'acqua, luci delle scale e luci dimmerabili).

Prima: Lo strumento vedeva una stanza vuota e diceva "Sicuro" (erroneamente).
Dopo: Lo strumento vedeva l'intera logica, controllava ogni possibile combinazione di input dei sensori e confermava che i programmi fossero effettivamente sicuri.
Velocità: Ha fatto tutto in meno di 70 millisecondi (più veloce di un battito di ciglia umano).
Sicurezza: Non ha rotto il vecchio strumento. Gli 11 programmi che già funzionavano con gli elenchi testuali funzionavano perfettamente.

Cosa non può ancora fare (Le Limitazioni)

Il documento è onesto riguardo a ciò che il detective fatica ancora a gestire:

Timer Complessi: Se un piolo coinvolge un timer (ad esempio, "Aspetta 5 secondi, poi accendi"), lo strumento attualmente ignora la parte di "attesa" e la tratta come un indovino casuale. È sicuro, ma non comprende la tempistica.
Mappe Annidate: Alcuni diagrammi complessi nascondono mappe più piccole all'interno di altre sezioni (come azioni all'interno di un passaggio). Il detective a volte perde di vista queste stanze nascoste.

Riassunto

In breve, gli autori hanno costruito un traduttore che permette al software di controllo della sicurezza di poter finalmente "leggere" i diagrammi a scala visivi utilizzati dai moderni software industriali. Hanno trasformato uno strumento che diceva ciecamente "Tutto va bene" in uno strumento che capisce davvero la logica e può provare che la macchina non si romperà o non farà male a nessuno.

Sintesi Tecnica: ESBMC-GraphPLC

Enunciato del Problema
Il documento affronta una lacuna critica nella verifica formale di programmi per Programmable Logic Controller (PLC) utilizzando lo strumento ESBMC-PLC. Sebbene ESBMC-PLC supportasse con successo il formato testuale di PLCopen XML (tc6_0201), non era in grado di elaborare correttamente il formato grafico, che è il formato di esportazione nativo per i principali ambienti di sviluppo come CONTROLLINO, Beremiz e OpenPLC Editor.

Nel formato grafico, la logica Ladder Diagram (LD) è codificata come un grafo diretto di connessioni localId e refLocalId piuttosto che come elementi <rung> espliciti. Il parser esistente rilevava questi file ma non trovava alcun rung, risultando in una rappresentazione intermedia (IR) GOTO vuota. Di conseguenza, tutte le variabili rimanevano inizializzate a zero, causando una verifica riuscita in modo vacuo: le proprietà erano soddisfatte trivialmente perché non veniva generata alcuna logica. Ciò non forniva alcuna garanzia reale riguardo alla sicurezza della logica del PLC.

Metodologia
Gli autori introducono ESBMC-GraphPLC, un modulo che colma questa lacuna implementando un risolutore basato sulla Ricerca in Profondità (DFS) per ricostruire la logica dei rung dal grafo delle connessioni grafiche. La metodologia comprende tre componenti principali:

Risolutore LD Grafico e Estrazione dei Rung:
- Il sistema analizza il grafo localId/refLocalId per identificare i percorsi dal leftPowerRail verso ogni coil.
- Attraversa il grafo per estrarre sequenze di contatti, convertendoli in congiunzioni booleane.
- Intuizione sull'Ordinamento Critico: Per aderire alla semantica del ciclo di scansione IEC 61131-3, l'algoritmo ordina l'elaborazione delle bobine (coil) in base alla sequenza delle voci refLocalId nella lista connectionPointIn del rightPowerRail. Ciò assicura che le bobine SET siano elaborate prima delle bobine RESET all'interno dello stesso ciclo di scansione, preservando il corretto comportamento di latch.
Inferenza I/O a Tre Livelli:
Per modellare correttamente gli input (risampionamento nondeterministico) e gli output (stato persistente), lo strumento impiega uno schema di classificazione a tre livelli:
- Livello 1: Utilizza indirizzi hardware espliciti IEC 61131-3 (%IX per gli input, %QX per gli output).
- Livello 2: Applica un'analisi euristica per programmi privi di indirizzi, classificando le variabili che appaiono solo come contatti come input e quelle che appaiono solo come bobine come output.
- Livello 3: Tratta le variabili non classificate come stato interno persistente.
Strategia di Implementazione:
La soluzione è implementata interamente nel parser del frontend (plcopen_xml_parser.cpp, +274 righe). Richiede zero modifiche al backend di ESBMC, inclusi l'encoder GOTO IR, il motore di k-induction, il solver SMT Z3 o l'encoder delle proprietà. Il risolutore produce una lista di RungNode standard, identica alla struttura prodotta dal parser testuale.

Contributi Chiave

Modello Formale: Una definizione formale del grafo di connessione LD grafico e un teorema di correttezza che dimostra che i percorsi estratti tramite DFS sono equivalenti alla semantica del ciclo di scansione IEC 61131-3.
Soluzione Algoritmica: La prima implementazione open-source di un estrattore di rung basato su DFS per PLCopen XML grafico che gestisce correttamente l'ordinamento SET/RESET.
Compatibilità Retroattiva: L'estensione preserva tutte le funzionalità esistenti per i benchmark LD testuali con zero regressioni.
Artefatto: Un artefatto completo e riproducibile che include lo strumento, i benchmark e un prototipo Python per la validazione.

Risultati Sperimentali
Lo strumento è stato valutato su 3 programmi LD grafici esportati da CONTROLLINO e OpenPLC Editor:

Controllo Acqua (water_control): 5 rung (2 SET, 3 RESET).
Luce Scala (stairs_light): 6 rung (2 SET, 2 RESET, 2 semplici).
Dimmer Luce (dimmer_light_control): 4 rung (semplici).

Esiti:

Completezza IR: Tutti i 3 programmi sono passati dalla produzione di una "Empty IR" (vacua) a una "Full IR" contenente input nondeterministici e logica completa dei rung.
Verifica: Tutti i 3 programmi sono stati verificati come SAFE a $k=2$ in meno di 70 ms (tempi mediani: 50ms, 40ms, 60ms).
Regressione: Gli 11 benchmark LD testuali originali di ESBMC-PLC hanno prodotto risultati identici, confermando l'assenza di regressioni.

Limitazioni e Ambito
Il documento nota esplicitamente che l'attuale risolutore non preserva la semantica dei blocchi funzione (timer, contatori, comparatori) all'interno dei percorsi dei rung. Se un rung dipende da un blocco funzione, lo strumento tratta l'uscita del blocco come un termine nondeterministico (sovra-approssimazione sicura/sound over-approximation) o, in casi specifici come l'esempio beremiz_traffic_light, la logica collassa in una costante. Due esempi di Beremiz sono stati esclusi dai risultati principali per evitare di riportare sentenze "SAFE" fuorvianti per programmi in cui la semantica temporale è andata perduta.

Significatività
Il documento afferma che ESBMC-GraphPLC consente la verifica formale non vacua e sound di programmi PLCopen XML grafici, che sono lo standard di output dei moderni ambienti di sviluppo PLC. Chiudendo il divario tra le esportazioni grafiche e il model checking basato su SMT, lo strumento permette agli ingegneri dell'automazione di verificare le proprietà di sicurezza (ad esempio, controllo pompe, semafori) senza una conversione manuale in formati testuali. Gli autori sottolineano che, sebbene l'attuale implementazione gestisca efficacemente le reti di contatti/bobine con latch SET/RESET, è necessario un lavoro futuro per integrare la semantica dei blocchi funzione per supportare la logica di controllo sequenziale più complessa.