ESBMC-Arduino: Bridging the Hardware-Software Gap in Industrial Control Verification
Formal verification meets real-world sensor constraints on resource-limited microcontrollers.
1The Verification Gap in Industrial PLCs
Existing open-source verifiers check IEC 61131-3 programs using abstract scan-cycle models with unbounded integer assumptions. Yet real systems on 8/16-bit MCUs like Arduino process sensor readings constrained by ADC resolution. This gap renders naive bit-width-aware verification unreliable for physical deployments.
2Cost of False Alarms
Tests on 123 real programs showed 16-bit overflow checks without hardware input models produced 44% false alarms (54/123) while finding zero genuine defects. The verifier explored sensor values beyond physical ADC capabilities, creating noise that could unnecessarily block safety actions.
3Physical-Digital Disconnect
The critical risk lies where finite-width arithmetic scales sensor readings into actuator commands. Silent overflows here may suppress safety actions like high-level alarms. Conversely, unbounded input models fabricate alarms no physical environment could trigger.
4Hardware-Faithful Solution
The paper presents a novel verification approach for open hardware: A declarative HAL descriptor (bit width, ADC/PWM resolution, I/O bindings) paired with sound lowering that interprets arithmetic at target width and constrains inputs to hardware-realizable ranges.
5ArduinoTool Implementation
Integrated into ESBMC's Ladder Diagram frontend, ArduinoTool derives HAL parameters from official cores. On the 123-program corpus, the HAL annotator eliminated all 54 false alarms while preserving robustness proofs. A controlled corpus demonstrates rare width-dependent defects with realizable witnesses.
6Industrial IoT Security Impact
This work overcomes practical barriers in verifying cyber-physical systems. By reducing false positives while modeling true hardware behavior in resource-constrained environments, it advances industrial IoT security where computation meets physical processes.