💬 NLP

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

Este artículo presenta ESBMC-PLC, el primer verificador formal de código abierto que soporta nativamente programas de Diagrama de Escalera IEC 61131-3 mediante la traducción de los mismos a una representación intermedia para la verificación de modelos basada en SMT, verificando así con éxito propiedades de seguridad y detectando errores en diversos referentes industriales mientras aborda brechas de investigación clave en el campo.

Autores originales: Pierre Dantas, Lucas Cordeiro, Waldir Junior

Publicado 2026-06-16

📖 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 una planta de fábrica donde máquinas gigantes, mezcladores químicos y señales de tren son controlados por un cerebro diminuto e incansable llamado PLC (Controlador Lógico Programable). Estas máquinas funcionan con un tipo especial de manual de instrucciones llamado Diagrama de Escalera (Ladder Diagram). Piensa en esto como un dibujo de una escalera donde cada "peldaño" es una regla: "Si la luz roja está encendida Y el botón se presiona, entonces enciende el motor".

Durante décadas, los ingenieros han escrito estas reglas dibujándolas, no escribiendo código. Esto hizo que fuera muy difícil para los "inspectores de seguridad" modernos (herramientas de verificación formal) comprobar si las reglas eran perfectas, porque los inspectores solo entendían el código escrito, no los dibujos.

Este artículo presenta ESBMC-PLC, una nueva herramienta que actúa como un traductor universal y un inspector de seguridad superestricto al mismo tiempo.

Así es como funciona, utilizando analogías sencillas:

1. El Traductor (La "Piedra de Rosetta")

Antes de esta herramienta, no podías pedirle a una computadora que revisara un dibujo. ESBMC-PLC toma el "Diagrama de Escalera" gráfico (el dibujo) y lo traduce instantáneamente a un lenguaje que la computadora entiende (un código intermedio basado en texto).

La Analogía: Imagina que tienes una receta escrita en un cuaderno de bocetos con dibujos de los ingredientes. ESBMC-PLC es el chef que mira los dibujos y escribe instantáneamente las instrucciones exactas en texto: "Añada 2 tazas de harina, luego revuelva". Ahora, la computadora puede leer la receta.

2. El Simulador (El "Bucle de Viaje en el Tiempo")

Un PLC no solo se ejecuta una vez; funciona en un bucle, revisando sensores y cambiando salidas miles de veces por segundo.

La Analogía: La mayoría de las comprobaciones de seguridad miran un solo momento en el tiempo. ESBMC-PLC es como un simulador de viaje en el tiempo que ejecuta el "día" de la fábrica una y otra vez. Pero en lugar de solo reproducir un día específico, simula cada día posible a la vez. Se pregunta: "¿Qué pasa si el sensor se rompe? ¿Qué pasa si el botón se presiona dos veces? ¿Qué pasa si la energía parpadea?". Revisa cada combinación de eventos para ver si puede ocurrir un desastre.

3. La Prueba "Ilimitada" (La "Garantía de Por Siempre")

Las herramientas antiguas solo podían comprobar un número limitado de pasos (como revisar los primeros 100 días de vida de una fábrica). Si un error ocurría en el día 101, lo pasarían por alto.

La Analogía: ESBMC-PLC utiliza un truque matemático especial llamado k-inducción. En lugar de contar los días uno por uno, demuestra una regla que dice: "Si la fábrica es segura hoy, y se siguen las reglas, será segura mañana, pasado mañana y para siempre". Ofrece una garantía de por siempre de que la máquina nunca fallará, siempre que se sigan las reglas.

4. El Lenguaje "Sin Lógica" (La "Lista de Verificación en Lenguaje Sencillo")

Normalmente, para pedirle a una computadora que verifique la seguridad, tenías que conocer la lógica matemática compleja (lógica temporal).

La Analogía: ESBMC-PLC permite a los ingenieros escribir reglas de seguridad en una simple lista de verificación YAML (como una lista de tareas):
- En lugar de: "Para todo tiempo t, si A es verdadero entonces B debe ser falso".
- Escribes: "El motor y el interruptor de reversa nunca deben estar encendidos al mismo tiempo".
  La herramienta entiende este lenguaje sencillo y lo comprueba automáticamente.

¿Qué Encontraron?

Los autores probaron esta herramienta en 13 programas de fábrica diferentes, que iban desde controles de motores simples hasta semáforos complejos y bombas de agua. Utilizaron programas de proveedores del mundo real (como CONTROLLINO y MathWorks) que no fueron diseñados para ser probados, solo para ver si la herramienta podía manejarlos.

Los Resultados:
- 100% de Precisión: Identificó correctamente cada programa seguro y cada programa inseguro.
- Encontró Errores Ocultos: Encontró 8 errores específicos que las pruebas estándar pasaron por alto. Por ejemplo, encontró un escenario donde un botón de parada de emergencia apagaba la máquina pero no lograba reiniciar un temporizador, lo que causaba que la máquina se reiniciara inmediatamente cuando se soltaba el botón.
- Velocidad: Comprobó todos estos programas en menos de 60 milisegundos (más rápido que un parpadeo humano).

La Conclusión

Este artículo presenta la primera herramienta de código abierto que puede tomar un dibujo industrial estándar (Diagrama de Escalera), traducirlo y demostrar matemáticamente que es seguro para siempre. Cierra la brecha entre la forma gráfica tradicional en que los ingenieros diseñan máquinas y la forma matemática de alta tecnología en que las computadoras verifican la seguridad.

Nota Importante: El artículo afirma que esto funciona para las partes "centrales" específicas de la programación industrial (lógica booleana, temporizadores, contadores). Todavía no maneja características complejas como números de punto flotante o arreglos de datos avanzados, pero para la gran mayoría de la lógica crítica de seguridad, funciona perfectamente y está listo para su uso hoy mismo.

Resumen Técnico: ESBMC-PLC

Planteamiento del Problema

Los Controladores Lógicos Programables (PLC) son críticos para la seguridad industrial, sin embargo, la notación de programación dominante, el Diagrama de Escalera (LD) estandarizado en IEC 61131-3, permanece en gran medida ausente del ecosistema de verificación formal. Las soluciones basadas en Satisfacibilidad de Teorías Modulares (SMT), como los verificadores de modelos ESBMC, han madurado para software de propósito general (C, Rust, Python), pero no pueden procesar directamente la notación gráfica de "escalón y bobina" (rung-and-coil) de LD. Las soluciones existentes requieren una traducción manual a lenguajes textuales (lo que introduce riesgos de fidelidad), dependen de herramientas propietarias o carecen de soporte para pruebas de seguridad no acotadas. En consecuencia, la lógica de seguridad crítica de la industria escapa a la rigurosa verificación matemática disponible para otros dominios de software, dejando los sistemas vulnerables a defectos de diseño e inyecciones de código malicioso como las Bombas de Lógica de Escalera (LLB).

Metodología

El artículo presenta ESBMC-PLC, un verificador formal de código abierto implementado como un nuevo frontend para el Verificador de Modelos de Límite de Contexto Eficiente basado en SMT (ESBMC). La metodología se centra en un pipeline de traducción directa desde PLCopen XML (el formato de intercambio abierto para LD) hacia la Representación Intermedia (IR) GOTO de ESBMC.

Arquitectura Central

Parsing de Entrada: La herramienta acepta archivos PLCopen XML (formatos tanto textuales como gráficos tc6_0201) exportados por los principales proveedores (Siemens, Rockwell, CODESYS, OpenPLC). Reconstruye la topología del circuito a partir de IDs de referencia sin necesidad de edición manual.
Traducción a GOTO-IR:
- Modelado del Ciclo de Escaneo: El modelo de ejecución del PLC se codifica como un bucle while(true).
- Gestión de Estado: Las variables de entrada se vuelven a muestrear de forma no determinista en cada iteración (modelando un entorno de sensores de mundo abierto). Las bobinas de salida y los marcadores internos se modelan como variables estáticas persistentes, preservando el estado a través de los ciclos de escaneo.
- Mapeo de Elementos: Los elementos de LD (contactos XIC/XIO, bobinas OTE/OTL/OTU, temporizadores TON/TOF/TP, contadores CTU/CTD) se traducen en operaciones GOTO-IR. Las reglas de traducción están diseñadas para coincidir con la semántica formal definida por Ebnenasir [9], particularmente respecto a la prioridad de enclavamiento (OTL/OTU) y los contadores activados por flanco.
- Tipos de Datos: Los tipos IEC 61131-3 se mapean a sus equivalentes en C más pequeños (por ejemplo, BOOL a bool, TIME a uint32_t que representa milisegundos).
Especificación de Propiedades: Un lenguaje basado en YAML permite a los ingenieros especificar cinco tipos de propiedades de seguridad sin necesidad de conocimientos en lógica temporal: mutual_exclusion (exclusión mutua), invariant (invariante), absence (ausencia), response (respuesta) y reachability (alcanzabilidad).
Motor de Verificación: El backend utiliza ESBMC con el solver SMT Z3. Soporta:
- BMC Incremental: Para la búsqueda rápida de errores en programas inseguros.
- k-Inducción: Para pruebas de seguridad no acotadas, verificando propiedades para todos los posibles ciclos de escaneo sin necesidad de desenrollado manual de bucles.

Principales Contribuciones

Primer Frontend Nativo de LD de Código Abierto: ESBMC-PLC es la primera herramienta de código abierto que acepta nativamente programas LD en formato PLCopen XML estándar, eliminando la necesidad de traducción manual a C o ST.
Pruebas No Acotadas para LD: Es la primera herramienta en aplicar k-inducción a programas LD, permitiendo pruebas de seguridad no acotadas en lugar de depender únicamente de la verificación de modelos acotada.
Contraejemplos Accionables: La herramienta genera contraejemplos que hacen referencia a los nombres originales de las variables de LD, lo que los hace directamente interpretables por ingenieros de automatización.
Análisis de Brechas Sistemático: Un estudio de 22 investigaciones (2020–2026) identificó cuatro brechas de investigación; ESBMC-PLC aborda directamente la falta de un traductor de LD a formal de código abierto y la ausencia de un frontend de ESBMC para IEC 61131-3.
Suite de Benchmarks: Los autores introdujeron una suite de 13 benchmarks que abarcan seis dominios industriales y tres fuentes (originales, sintéticos y programas de proveedores del mundo real), incluyendo programas sin modificaciones de CONTROLLINO y MathWorks.

Resultados Experimentales

La evaluación se realizó sobre 13 benchmarks (7 seguros, 6 inseguros) en seis dominios industriales (motores, transporte, seguridad, infraestructura, industria alimentaria, edificios).

Precisión de Clasificación: ESBMC-PLC clasificó correctamente todos los 13 benchmarks con cero falsos positivos y cero falsos negativos. Esto incluyó 4 programas de proveedores independientes (Categoría C) que no fueron pre-etiquetados por los autores.
Detección de Errores: La herramienta identificó 8 errores distintos en las variantes inseguras. Estos incluyeron:
- Fallo al resetear temporizadores tras una parada de emergencia (CS2).
- Lógica de reset que anula las señales de apagado de emergencia (CS3).
- Falta de enclavamientos para la activación simultánea de fases en semáforos (CS4).
- Condiciones de carrera donde las señales de puerta abierta se activan en el mismo ciclo de escaneo que el arranque del motor (CS8).
- Activación simultánea de bombas y válvulas bajo condiciones de fallo de sensor (CS12).
Rendimiento: Todas las 61 comprobaciones de propiedades se completaron en menos de 60 ms en Apple Silicon (aarch64).
Pruebas No Acotadas: Los 7 programas seguros fueron verificados mediante k-inducción (convergiendo en $k=2$ ), proporcionando garantías de seguridad incondicionales.
Validación en el Mundo Real: La herramienta parseó y verificó con éxito programas del mundo real del repositorio CONTROLLINO y de la documentación de MathWorks Simulink PLC Coder sin preprocesamiento.

Significado y Reivindicaciones

El artículo afirma que ESBMC-PLC demuestra que la verificación formal de la Lógica de Escalera de PLC industriales es una operación práctica, de código abierto y de sub-segundo accesible para los ingenieros de automatización.

Posicionamiento Único: A diferencia del estado del arte PLCverif (que depende de CBMC y requiere entrada ST/SCL), ESBMC-PLC es la única herramienta de código abierto que combina entrada nativa de LD, pruebas no acotadas mediante k-inducción y semántica de vectores de bits SMT.
Impacto Práctico: Al detectar errores que las pruebas funcionales convencionales pasan por alto (como escenarios de fallo de sensores y condiciones de carrera dependientes del orden del ciclo de escaneo), la herramienta aborda brechas de seguridad críticas en los sistemas de control industrial.
Limitaciones y Alcance: Los autores señalan modestamente que las reglas de traducción han sido validadas empíricamente contra la semántica de Ebnenasir, pero no se han probado formalmente como equivalentes al estándar IEC 61131-3. La implementación actual cubre un subconjunto central de constructos (excluyendo REAL/FLOAT, cadenas, arreglos y programas multi-POU) y aún no soporta extensiones específicas de proveedores como las tareas de interrupción.

El artículo concluye que ESBMC-PLC cierra brechas de investigación significativas en la verificación de PLC y sugiere que una plataforma unificada que integre el frontend de LD de ESBMC-PLC con el pipeline de ST de PLCverif representa una dirección futura lógica para la verificación de grado industrial.