ESBMC-Arduino：填补形式验证部署鸿沟

ESBMC-Arduino: Closing the Deployment Gap for Formal Verification

OpenPLC、Arduino OPTA 等开源硬件正将 IEC 61131-3 带入低成本微控制器领域，但现有的 ESBMC-PLC 等验证工具却因脱离硬件现实而频频误报。研究团队发现，在 123 个真实程序中，忽视 16 位整数溢出和有限分辨率 ADC 输入模型，竟导致 44% 的虚假警报，却漏掉真正的安全隐患。为此，他们推出了 ArduinoTool，通过声明式硬件抽象层（HAL）精准模拟目标硬件的位宽与传感器范围。这一改进不仅消除了所有误报，还能捕捉到那些仅在特定硬件约束下才会触发的罕见缺陷，真正实现了从理论验证到物理部署的无缝衔接。

"由于鸿沟存在于计算与物理过程的交汇点——即有界的传感器读数经有限位宽算术运算转化为执行指令的过程，溢出可能会静默地抑制安全动作，例如高级警报。"