Hardware-Aware Model Fixes False Alarms in PLC Verification for Arduino
A hardware-aware verification method eliminates false alarms in formal analysis of IEC 61131-3 PLC code deployed on Arduino-based industrial controllers.
Open-source formal verifiers for IEC 61131-3 PLC programs, such as ESBMC-PLC, prove safety over an abstract scan-cycle model with idealized unbounded integers. But real deployments — OpenPLC, Arduino OPTA, CONTROLLINO, and Industrial Shields M-Duino — run on resource-constrained microcontrollers with 16-bit words and finite-resolution ADCs, creating a gap between the verified model and the physical system.
Across 123 real-world programs, naive width-aware overflow checking without a hardware input model produced 44% false alarms (54 of 123) and found no genuine defects, because it explored sensor values no ADC could ever produce. This matters because an overflow at the boundary between computation and the physical process can silently suppress a safety action, such as a high-level alarm, while unbounded input models can fabricate alarms no environment could trigger.
The researchers propose a declarative hardware abstraction layer (HAL) descriptor capturing width, ADC/PWM resolution, and I/O binding, paired with a sound lowering that constrains inputs to hardware-realizable ranges. Instantiated for Arduino as ArduinoTool and integrated into ESBMC's Ladder Diagram frontend, the approach derives HAL parameters directly from official hardware cores.
On the 123-program corpus, the HAL annotator eliminated all 54 false alarms while preserving robustness proofs, and a controlled corpus confirmed it can still catch rare width-dependent defects with realizable witnesses — a meaningful step toward trustworthy formal verification for low-cost industrial control hardware used in ICS security research.