💬 NLP

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

Este artículo presenta ESBMC-GraphPLC, una herramienta de verificación formal que resuelve la brecha en el manejo de diagramas de escalera XML de tipo PLCopen mediante la implementación de un resolvedor basado en DFS para convertir la lógica de peldaños basada en grafos en una representación intermedia GOTO válida para la comprobación de modelos basada en SMT, permitiendo así la verificación correcta de programas provenientes de editores como CONTROLLINO y OpenPLC Editor sin afectar el soporte existente para el formato textual.

Autores originales: Pierre Dantas, Lucas Cordeiro, Waldir Junior

Publicado 2026-06-19

📖 5 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Pierre Dantas, Lucas Cordeiro, Waldir Junior

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina un Controlador Lógico Programable (PLC) como el cerebro de una máquina de fábrica, como una bomba de agua o un semáforo. Para decirle a este cerebro qué hacer, los ingenieros dibujan Diagramas de Escalera. Estos parecen escaleras eléctricas con peldaños, donde cada peldaño es una regla: "Si el tanque de agua está lleno, apaga la bomba".

Durante mucho tiempo, hubo dos formas de guardar estos dibujos de escalera en una computadora:

La Lista de Texto: Una lista simple, paso a paso, de instrucciones (como una receta).
El Mapa Gráfico: Un mapa visual donde las piezas están conectadas por cables invisibles, identificados por números de ID (como un mapa de metro donde las estaciones están conectadas por líneas).

El Problema: El Programa "Fantasma"

Los investigadores tenían una herramienta poderosa llamada ESBMC-PLC que podía verificar si estos programas tenían errores de seguridad. Funcionaba perfectamente con el formato de Lista de Texto.

Sin embargo, cuando le suministraron el formato de Mapa Gráfico (que es lo que el software moderno como CONTROLLINO y OpenPLC realmente utiliza), la herramienta se confundió. Miraba el mapa, veía los números de ID y los cables, pero no podía entender cómo se conectaban.

Como no podía leer el mapa, asumía que no estaba pasando nada. Pensaba que cada interruptor estaba apagado y que cada bomba estaba detenida.

El Resultado: La herramienta decía: "¡Todo es seguro!"
La Trampa: Estaba mintiendo. No era segura porque la lógica faltaba; era "segura" porque la herramienta estaba mirando una habitación vacía. Esto se llama verificación vacua — es como decir que una puerta cerrada es segura porque olvidaste revisar si hay una ventana abierta.

La Solución: ESBMC-GraphPLC

Los autores construyeron un nuevo módulo llamado ESBMC-GraphPLC para solucionar esto. Piensa en esto como contratar a un detective para que camine a través del mapa gráfico y lo traduzca de nuevo a un lenguaje que el verificador de seguridad entienda.

Aquí es cómo trabaja su "detective", usando analogías simples:

1. El Detective con una Linterna (Algoritmo DFS)
La herramienta utiliza un método llamado Búsqueda en Profundidad (DFS). Imagina a un detective caminando a través de un laberinto de cables. Comienza en el lado izquierdo de la escalera (la fuente de energía) y sigue cada posible camino hacia el lado derecho.

Rastrea cada conexión de cable.
Anota cada interruptor (contacto) que pasa.
Se detiene cuando llega al dispositivo (la bobina/bomba).
Al hacer esto, reconstruye la lógica exacta del peldaño de la escalera, convirtiendo el mapa visual de nuevo en una regla clara de "Si-Entonces".

2. El Agente de Tránsito (El orden importa)
En estos diagramas, a veces tienes un interruptor de "Set" (encender) y un interruptor de "Reset" (apagar) para el mismo dispositivo. ¡El orden importa!

Si el "Reset" ocurre después del "Set" en el mismo milisegundo, el dispositivo permanece apagado.
Si el "Set" ocurre después del "Reset", el dispositivo permanece encendido.
La nueva herramienta mira una lista específica en el archivo (la secuencia rightPowerRail) para ver qué interruptor viene primero, actuando como un agente de tránsito que asegura que el coche "Set" pase antes que el coche "Reset". Esto garantiza que la lógica coincida con cómo se comportan las máquinas reales.

3. El Juego de Adivinanza (Inferencia de E/S)
A veces el mapa no dice cuáles cables son "Entradas" (sensores) y cuáles son "Salidas" (motores). La herramienta utiliza un juego de adivinación de tres pasos:

Paso 1: Buscar etiquetas de dirección oficiales (como %IX para entradas). Si se encuentran, es exacto.
Paso 2: Si no hay etiquetas, observar el comportamiento. Si un cable es solo usado como un interruptor, es probablemente una entrada. Si es solo usado para encender algo, es probablemente una salida.
Paso 3: Si aún no está seguro, tratarlo como una "variable misteriosa" que podría ser cualquier cosa. Esta es una apuesta segura porque verifica todas las posibilidades, asegurando que nada se pase por alto.

Los Resultados

El equipo probó este nuevo detective en tres programas del mundo real (bombas de agua, luces de escalera y luces de atenuación).

Antes: La herramienta veía una habitación vacía y decía "Seguro" (incorrectamente).
Después: La herramienta vio la lógica completa, revisó todas las combinaciones posibles de entradas de sensores y confirmó que los programas eran realmente seguros.
Velocidad: Lo hizo en menos de 70 milisegundos (más rápido que un parpadeo humano).
Seguridad: No rompió la herramienta antigua. Los 11 programas que ya funcionaban con listas de texto funcionaron perfectamente.

Lo que aún no puede hacer (Las Limitaciones)

El artículo es honesto sobre con qué todavía tiene dificultades el detective:

Temporizadores Complejos: Si un peldaño involucra un temporizador (por ejemplo, "Esperar 5 segundos, luego encender"), la herramienta actualmente ignora la parte de "esperar" y la trata como una suposición aleatoria. Es seguro, pero no entiende el tiempo.
Mapas Anidados: Algunos diagramas complejos esconden mapas más pequeños dentro de otras secciones (como acciones dentro de un paso). El detective a veces pierde de vista estas habitaciones ocultas.

Resumen

En resumen, los autores construyeron un traductor que permite al software de verificación de seguridad finalmente "leer" los diagramas de escalera visuales utilizados por el software industrial moderno. Convirtieron una herramienta que ciegamente decía "Todo está bien" en una herramienta que realmente entiende la lógica y puede probar que la máquina no se romperá ni hará daño a nadie.

Resumen Técnico: ESBMC-GraphPLC

Planteamiento del Problema
El artículo aborda una brecha crítica en la verificación formal de programas de Controlador Lógico Programable (PLC) utilizando la herramienta ESBMC-PLC. Si bien ESBMC-PLC soportaba con éxito el formato textual de PLCopen XML (tc6_0201), fallaba al procesar correctamente el formato gráfico, que es el formato de exportación nativo de entornos de desarrollo principales como CONTROLLINO, Beremiz y OpenPLC Editor.

En el formato gráfico, la lógica de Diagrama de Escalera (LD) se codifica como un grafo dirigido de conexiones localId y refLocalId en lugar de elementos <rung> explícitos. El analizador existente detectaba estos archivos pero no encontraba renglones (rungs), lo que resultaba en una Representación Intermedia (IR) de GOTO vacía. En consecuencia, todas las variables permanecían con inicialización en cero, causando que la verificación tuviera éxito de forma vacua: las propiedades se cumplían trivialmente porque no se generaba ninguna lógica. Esto no proporcionaba ninguna garantía real sobre la seguridad de la lógica del PLC.

Metodología
Los autores presentan ESBMC-GraphPLC, un módulo que cierra esta brecha mediante la implementación de un resolvedor basado en Búsqueda en Profundidad (DFS) para reconstruir la lógica de los renglones a partir del grafo de conexiones gráficas. La metodología consta de tres componentes principales:

Resolución de LD Gráfico y Extracción de Renglones:
- El sistema analiza el grafo localId/refLocalId para identificar rutas desde el riel de potencia izquierdo (leftPowerRail) hacia cada bobina (coil).
- Recorre el grafo para extraer secuencias de contactos, convirtiéndolas en conjunciones booleanas.
- Perspectiva Crítica de Ordenamiento: Para adherirse a la semántica del ciclo de escaneo de la norma IEC 61131-3, el algoritmo ordena el procesamiento de las bobinas basándose en la secuencia de entradas connectionPointIn del rightPowerRail. Esto asegura que las bobinas SET se procesen antes que las bobinas RESET dentro del mismo ciclo de escaneo, preservando el comportamiento de enclavamiento correcto.
Inferencia de E/S de Tres Niveles:
Para modelar correctamente las entradas (remuestreo no determinista) y las salidas (estado persistente), la herramienta emplea un esquema de clasificación por niveles:
- Nivel 1: Utiliza direcciones de hardware explícitas de IEC 61131-3 (%IX para entradas, %QX para salidas).
- Nivel 2: Aplica un análisis heurístico para programas sin direcciones, clasificando las variables que aparecen solo como contactos como entradas y aquellas que aparecen solo como bobinas como salidas.
- Nivel 3: Trata las variables no clasificadas como estado interno persistente.
Estrategia de Implementación:
La solución se implementa íntegramente dentro del analizador frontal (plcopen_xml_parser.cpp, +274 líneas). Requiere cero cambios en el backend de ESBMC, incluyendo el codificador de IR de GOTO, el motor de k-inducción, el solver SMT Z3 o el codificador de propiedades. El resolvedor genera una lista de RungNode estándar, idéntica a la estructura producida por el analizador textual.

Contribuciones Clave

Modelo Formal: Una definición formal del grafo de conexiones de LD gráfico y un teorema de solidez que demuestra que las rutas extraídas por DFS son equivalentes a la semántica de ciclo de escaneo de IEC 61131-3.
Solución Algorítmica: La primera implementación de código abierto de un extractor de renglones basado en DFS para PLCopen XML gráfico que maneja correctamente el ordenamiento SET/RESET.
Compatibilidad Hacia Atrás: La extensión preserva toda la funcionalidad existente para los benchmarks de LD textuales con cero regresiones.
Artefacto: Un artefacto completo y reproducible que incluye la herramienta, los benchmarks y un prototipo en Python para validación.

Resultados Experimentales
La herramienta fue evaluada en 3 programas de LD gráficos exportados desde CONTROLLINO y OpenPLC Editor:

Control de Agua (water_control): 5 renglones (2 SET, 3 RESET).
Luz de Escalera (stairs_light): 6 renglones (2 SET, 2 RESET, 2 simples).
Control de Atenuación de Luz (dimmer_light_control): 4 renglones (simples).

Resultados:

Integridad de la IR: Los 3 programas pasaron de producir una "IR Vacía" (vacua) a una "IR Completa" que contiene entradas no deterministas y lógica de renglón completa.
Verificación: Los 3 programas se verificaron como SEGUROS (SAFE) en $k=2$ en menos de 70 ms (tiempos medianos: 50ms, 40ms, 60ms).
Regresión: Los 11 benchmarks genuinos de LD textual produjeron resultados idénticos, confirmando cero regresiones.

Limitaciones y Alcance
El artículo señala explícitamente que el resolvedor actual no preserva la semántica de los bloques de función (temporizadores, contadores, comparadores) dentro de las rutas de los renglones. Si un renglón depende de un bloque de función, la herramienta trata la salida del bloque como un término no determinista (sobreaproximación sólida) o, en casos específicos como el ejemplo beremiz_traffic_light, la lógica colapsa a una constante. Dos ejemplos de Beremiz fueron excluidos de los resultados principales para evitar reportar veredictos "SAFE" engañosos en programas donde la semántica de tiempo se perdió.

Significancia
El artículo afirma que ESBMC-GraphPLC permite la verificación formal sólida y no vacua de los programas gráficos de PLCopen XML, que son el estándar de salida de los entornos de desarrollo de PLC modernos. Al cerrar la brecha entre las exportaciones gráficas y la verificación de modelos basada en SMT, la herramienta permite a los ingenieros de automatización verificar propiedades de seguridad (por ejemplo, control de bombas, semáforos) sin necesidad de conversión manual a formatos textuales. Los autores enfatizan que, si bien la implementación actual maneja eficazmente las redes de contactos/bobinas con enclavamientos SET/RESET, se requiere trabajo futuro para integrar la semántica de los bloques de función para soportar lógica de control secuencial más compleja.