Un equipo de investigación presenta ESBMC-Arduino, una extensión del verificador formal ESBMC orientada a programas de autómatas programables (PLC) que se ejecutan sobre hardware abierto inspirado en Arduino, como OpenPLC, Arduino OPTA, CONTROLLINO e Industrial Shields M-Duino. La herramienta nace para cerrar una brecha concreta: los verificadores previos, entre ellos ESBMC-PLC, demostraban propiedades de seguridad sobre un modelo abstracto de ciclo de escaneo con enteros no acotados, mientras que el artefacto real corre en microcontroladores de 16 bits (o 8 bits en Arduinos AVR) y recibe lecturas de sensores mediante un conversor analógico-digital (ADC) de resolución finita.
Los autores demuestran que esa brecha hace que la verificación con conciencia de ancho sea, en la práctica, incorrecta: al analizar 123 programas reales, comprobar el desbordamiento de 16 bits sin un modelo de entradas del hardware genera un 44 % de falsas alarmas (54 de 123) y no detecta defectos genuinos, porque explora valores de sensor que ningún ADC puede producir. La raíz del problema está en el punto en que el cómputo se encuentra con el proceso físico: una lectura acotada, escalada con aritmética de ancho finito hasta un comando de actuación. Un desbordamiento puede silenciar una acción de seguridad, como una alarma de nivel alto, y un modelo de entrada no acotado fabrica alarmas imposibles.
La solución propuesta es una verificación fiel al hardware para IEC 61131-3: una capa de abstracción de hardware (HAL) declarativa que describe el ancho de palabra, la resolución del ADC y del PWM y el binding de E/S, junto con un proceso de lowering (reducción tipada) que interpreta la aritmética en el ancho del dispositivo y restringe las entradas al rango realizable por el sensor. Como caso de estudio, los autores materializan esta idea en ArduinoTool, derivan sus parámetros HAL a partir de los cores oficiales de Arduino e integran el modelo de rangos de entrada en el frontend de diagramas ladder (LD) de ESBMC. Sobre el corpus de 123 programas, el anotador HAL elimina las 54 falsas alarmas conservando las pruebas de robustez, y un corpus controlado muestra los defectos dependientes del ancho que la herramienta detecta con testigos realizables por el hardware.