💬 NLP

ESBMC-PLC: Formal Verification of IEC 61131-3 Ladder Diagram Programs Using SMT-Based Model Checking

Questo articolo introduce ESBMC-PLC, il primo verificatore formale open-source che supporta nativamente i programmi Ladder Diagram IEC 61131-3 traducendoli in una rappresentazione intermedia per il model checking basato su SMT, verificando con successo proprietà di sicurezza e rilevando bug in diversi benchmark industriali pur affrontando le principali lacune di ricerca nel campo.

Autori originali: Pierre Dantas, Lucas Cordeiro, Waldir Junior

Pubblicato 2026-06-16

📖 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

Immaginate il pavimento di una fabbrica dove enormi macchinari, miscelatori chimici e segnali ferroviari sono controllati da un piccolo, instancabile cervello chiamato PLC (Programmable Logic Controller). Queste macchine funzionano grazie a un tipo speciale di manuale di istruzioni chiamato Ladder Diagram (Diagramma a Scaletta). Pensatelo come il disegno di una scala dove ogni "piolo" è una regola: "Se la luce rossa è accesa E il pulsante è premuto, allora accendi il motore".

Per decenni, gli ingegneri hanno scritto queste regole disegnandole, non scrivendo codice. Questo ha reso molto difficile per i moderni "ispettori della sicurezza" (strumenti di verifica formale) controllare se le regole fossero perfette, perché gli ispettori comprendevano solo il codice testuale, non i disegni.

Questo articolo presenta ESBMC-PLC, un nuovo strumento che funge sia da traduttore universale che da ispettore della sicurezza super rigoroso.

Ecco come funziona, utilizzando semplici analogie:

1. Il Traduttore (La "Stele di Rosetta")

Prima di questo strumento, non era possibile chiedere a un computer di controllare un disegno. ESBMC-PLC prende il "Ladder Diagram" grafico (il disegno) e lo traduce istantaneamente in un linguaggio che il computer comprende (un codice intermedio basato su testo).

L'analogia: Immaginate di avere una ricetta scritta in un taccuino con i disegni degli ingredienti. ESBMC-PLC è lo chef che guarda le immagini e scrive istantaneamente le istruzioni testuali esatte: "Aggiungi 2 tazze di farina, poi mescola". Ora il computer può leggere la ricetta.

2. Il Simulatore (Il "Ciclo del Viaggio nel Tempo")

Un PLC non si limita a eseguire un'azione una sola volta; funziona in un ciclo, controllando i sensori e cambiando gli output migliaia di volte al secondo.

L'analogia: La maggior parte dei controlli di sicurezza analizza un singolo momento nel tempo. ESBMC-PLC è come un simulatore di viaggi nel tempo che riproduce la "giornata" della fabbrica ancora e ancora. Ma invece di riprodurre semplicemente un giorno specifico, simula ogni possibile giorno contemporaneamente. Chiede: "E se il sensore si rompesse? E se il pulsante venisse premuto due volte? E se la corrente sfarfallasse?". Controlla ogni singola combinazione di eventi per vedere se può verificarsi un disastro.

3. La Prova "Unbounded" (La "Garanzia di Eternità")

I vecchi strumenti potevano controllare solo un numero limitato di passaggi (come controllare i primi 100 giorni di vita di una fabbrica). Se un bug si fosse verificato al giorno 101, lo avrebbero perso.

L'analogia: ESBC-MPLC utilizza un trucco matematico speciale chiamato k-induction. Invece di contare i giorni uno per uno, dimostra una regola che dice: "Se la fabbrica è sicura oggi, e le regole vengono seguite, sarà sicura domani, dopodomani e per sempre". Fornisce una garanzia di eternità che la macchina non si guasterà mai, a patto che le regole vengano rispettate.

4. Il Linguaggio "Senza Logica" (La "Lista di Controllo in Lingua Semplice")

Solitamente, per chiedere a un computer di controllare la sicurezza, era necessario conoscere la complessa logica temporale.

L'analogia: ESBMC-PLC permette agli ingegneri di scrivere le regole di sicurezza in un semplice elenco YAML (come una lista di cose da fare).
- Inveve di: "Per ogni tempo t, se A è vero allora B deve essere falso".
- Scrivete: "Il motore e l'interruttore di inversione non devono mai essere accesi contemporaneamente".
  Lo strumento comprende questa lingua semplice e controlla automaticamente.

Cosa hanno scoperto?

Gli autori hanno testato questo strumento su 13 diversi programmi di fabbrica, che vanno dai semplici controlli di un motore ai complessi semafori o alle pompe d'acqua. Hanno utilizzato programmi di fornitori reali (come CONTROLLINO e MathWorks) che non erano stati progettati per essere testati, solo per vedere se lo strumento potesse gestirli.

I Risultati:
- Accuratezza al 100%: Ha identificato correttamente ogni programma sicuro e ogni programma non sicuro.
- Trova Bug Nascosti: Ha trovato 8 bug specifici che i test standard avevano mancato. Ad esempio, ha trovato uno scenario in cui un pulsante di arresto di emergenza spegneva la macchina ma non riusciva a resettare un timer, causando il riavvio immediato della macchina quando il pulsante veniva rilasciato.
- Velocità: Ha controllato tutti questi programmi in meno di 60 millisecondi (più velocemente di un battito di ciglia umano).

In sintesi

Questo articolo presenta il primo strumento open-source in grado di prendere un normale disegno industriale (Ladder Diagram), tradurlo e dimostrare matematicamente che è sicuro per sempre. Colma il divario tra il modo grafico tradizionale con cui gli ingegneri progettano le macchine e il modo matematico ad alta tecnologia con cui i computer verificano la sicurezza.

Nota Importante: L'articolo afferma che questo funziona per le parti "core" specifiche della programmazione industriale (logica booleana, timer, contatori). Non gestisce ancora funzioni complesse come i numeri in virgola mobile o array di dati avanzati, ma per la stragrande maggioranza della logica critica per la sicurezza, funziona perfettamente ed è pronto per l'uso oggi stesso.

Riepilogo Tecnico: ESBMC-PLC

Definizione del Problema

I Programmabili Logici Industriali (PLC) sono critici per la sicurezza industriale, eppure la notazione di programmazione dominante, il Ladder Diagram (LD) standardizzato in IEC 61131-3, rimane ampiamente assente dall'ecosistema della verifica formale. I model checker basati su Satisfiability Modulo Theories (SMT), come ESBMC, si sono evoluti per software general-purpose (C, Rust, Python), ma non possono elaborare direttamente la notazione grafica "a riga e bobina" (rung-and-coil) tipica del LD. Le soluzioni esistenti richiedono o una traduzione manuale in linguaggi testuali (introducendo rischi di fedeltà), o si affidano a strumenti proprietari, o mancano del supporto per prove di sicurezza non limitate (unbounded). Di conseguenza, la logica industriale critica per la sicurezza sfugge alla rigorosa verifica matematica disponibile per altri domini software, lasciando i sistemi vulnerabili a difetti di progettazione e iniezioni di codice malevolo come le Ladder Logic Bombs (LLB).

Metodologia

Il documento presenta ESBMC-PLC, un verificatore formale open-source implementato come un nuovo frontend per l'Efficient SMT-based Context-Bounded Model Checker (ESBMC). La metodologia si basa su una pipeline di traduzione diretta da PLCopen XML (il formato di interscambio aperto per il LD) alla GOTO-Intermediate Representation (IR) interna di ESBMC.

Architettura Core

Parsing dell'Input: Lo strumento accetta file PLCopen XML (formati sia testuali che grafici tc6_0201) esportati dai principali vendor (Siemens, Rockwell, CODESYS, OpenPLC). Ricostruisce la topologia del circuito dai riferimenti ID senza necessità di editing manuale.
Traduzione in GOTO-IR:
- Modellazione del Ciclo di Scan: Il modello di esecuzione del PLC è codificato come un ciclo while(true).
- Gestione dello Stato: Le variabili di input vengono campionate nuovamente in modo non deterministico ad ogni iterazione (modellando un ambiente di sensori a mondo aperto). Le bobine di uscita e i marker interni sono modellati come variabili statiche persistenti, preservando lo stato attraverso i cicli di scan.
- Mappatura degli Elementi: Gli elementi LD (contatti XIC/XIO, bobine OTE/OTL/OTU, timer TON/TOF/TP, contatori CTU/CTD) sono tradotti in operazioni GOTO-IR. Le regole di traduzione sono progettate per corrispondere alle semantiche formali definite da Ebnenasir [9], in particolare riguardo alla priorità di latch (OTL/OTU) e ai contatori a trigger di bordo (edge-triggered).
- Tipi di Dato: I tipi IEC 61131-3 sono mappati nei loro equivalenti C più piccoli (ad esempio, BOOL in bool, TIME in uint32_t che rappresenta i millisecondi).
Specifica delle Proprietà: Un linguaggio basato su YAML consente agli ingegneri di specificare cinque tipi di proprietà di sicurezza senza competenze in logica temporale: mutual_exclusion, invariant, absence, response e reachability.
Motore di Verifica: Il backend utilizza ESBMC con il solver SMT Z3. Supporta:
- Incremental BMC: Per il rapido rilevamento di bug in programmi non sicuri.
- k-Induction: Per prove di sicurezza non limitate (unbounded), verificando le proprietà per tutti i possibili cicli di scan senza l'unrolling manuale dei loop.

Contributi Chiave

Primo Frontend Nativo Open-Source per LD: ESBMC-PLC è il primo strumento open-source che accetta nativamente programmi LD in formato PLCopen XML standard, eliminando la necessità di traduzioni manuali in C o ST.
Prove Unbounded per LD: È il primo strumento ad applicare la k-induzione ai programmi LD, consentendo prove di sicurezza non limitate anziché affidarsi esclusivamente al bounded model checking.
Controesempi Azionabili: Lo strumento genera controesempi che fanno riferimento ai nomi originali delle variabili LD, rendendoli direttamente interpretabili dagli ingegneri dell'automazione.
Analisi Sistematica dei Gap: Un sondaggio su 22 studi (2020–2026) ha identificato quattro lacune nella ricerca; ESBMC-PLC affronta direttamente la mancanza di un traduttore open-source da LD a formale e l'assenza di un frontend ESBMC per IEC 61131-3.
Suite di Benchmark: Gli autori hanno introdotto una suite di 13 benchmark che spaziano su sei domini industriali e tre fonti (originali, sintetici e programmi vendor reali), inclusi programmi non modificati di CONTROLLINO e MathWorks.

Risultati Sperimentali

La valutazione è stata condotta su 13 benchmark (7 sicuri, 6 non sicuri) in sei domini industriali (motori, trasporti, sicurezza, infrastrutture, industria alimentare, edifici).

Accuratezza di Classificazione: ESBMC-PLC ha classificato correttamente tutti i 13 benchmark con zero falsi positivi e zero falsi negativi. Ciò includeva 4 programmi vendor indipendenti (Categoria C) che non erano stati pre-etichettati dagli autori.
Rilevamento Bug: Lo strumento ha identificato 8 bug distinti nelle varianti non sicure. Questi includevano:
- Mancato reset dei timer all'arresto di emergenza (CS2).
- Logica di reset che sovrascrive i segnali di arresto di emergenza (CS3).
- Mancanza di interblocchi per l'attivazione simultanea di fasi nei semafori (CS4).
- Race condition in cui i segnali di porta aperta venivano attivati nello stesso ciclo di scan dell'avvio del motore (CS8).
- Attivazione simultanea di pompe e valvole in condizioni di guasto del sensore (CS12).
Prestazioni: Tutti i 61 controlli di proprietà sono stati completati in meno di 60 ms su Apple Silicon (aarch64).
Prove Unbounded: Tutti i 7 programmi sicuri sono stati verificati tramite k-induction (convergendo a $k=2$ ), fornendo garanzie di sicurezza incondizionate.
Validazione nel Mondo Reale: Lo strumento ha analizzato e verificato con successo programmi reali dal repository CONTROLLINO e dalla documentazione MathWorks Simulink PLC Coder senza pre-processing.

Significato e Rivendicazioni

Il documento afferma che ESBMC-PLC dimostra che la verifica formale della Ladder Logic dei PLC industriali è un'operazione pratica, open-source e sub-secondaria accessibile agli ingegneri dell'automazione.

Posizionamento Unico: A differenza dello stato dell'arte PLCverif (che si basa su CBMC e richiede input in ST/SCL), ESBMC-PLC è l'unico strumento open-source che combina input LD nativo, prove unbounded tramite k-induction e semantica bit-vector SMT.
Impatto Pratico: Rilevando bug che i test funzionali convenzionali perdono (come scenari di guasto dei sensori e race condition dipendenti dall'ordine del ciclo di scan), lo strumento affronta lacune critiche di sicurezza nei sistemi di controllo industriale.
Limitazioni e Ambito: Gli autori notano con modestia che le regole di traduzione sono validate empiricamente rispetto alle semantiche di Ebnenasir, ma non sono formalmente provate come equivalenti allo standard IEC 61131-3. L'implementazione attuale copre un sottoinsieme fondamentale di costrutti (escludendo REAL/FLOAT, stringhe, array e programmi multi-POU) e non supporta ancora estensioni specifiche dei vendor come i task di interrupt.

Il documento conclude che ESBMC-PLC colma significativi gap di ricerca e suggerisce che una piattaforma unificata che integri il frontend LD di ESBMC-PLC con la pipeline ST di PLCverif rappresenti una direzione futura logica per la verifica di grado industriale.