ESBMC-Arduino: cierra la brecha entre la verificación formal y el hardware real

ESBMC-Arduino: Closing the Deployment Gap for Formal Verification

OpenPLC, Arduino OPTA, CONTROLLINO y M-Duino de Industrial Shields llevan IEC 61131-3 a microcontroladores de bajo costo usados en automatización real e investigación de seguridad en sistemas de control industrial. Sin embargo, los verificadores de código abierto existentes, como ESBMC-PLC, prueban la seguridad sobre un modelo abstracto de ciclo de escaneo con enteros idealizados sin límites. Este artículo demuestra que esta brecha de implementación hace que la verificación ingenua sensible al ancho sea insound: en 123 programas reales, verificar el desbordamiento de 16 bits sin un modelo de entrada de hardware produce 44% de falsas alarmas (54/123) y no encuentra defectos reales, porque explora valores de sensor que ningún ADC puede producir. Presentan una verificación fiel al hardware para IEC 61131-3 en hardware abierto: una capa de abstracción de hardware declarativa (HAL) y una reducción sólida que interpreta la aritmética al ancho objetivo y restringe las entradas a rangos realizables por hardware. La instancian para Arduino como ArduinoTool, eliminando las 54 falsas alarmas y detectando defectos dependientes del ancho con testigos realizables.