ESBMC-Arduino: Closing the Deployment Gap for Formal Verification
5 hours ago
- #Open Hardware
- #Formal Verification
- #IEC 61131-3
- 本文介绍了ESBMC-Arduino，以弥合运行在微控制器（如Arduino）上的开源硬件PLC形式化验证中的部署差距。
- 文章强调，缺乏硬件输入模型的朴素宽度感知验证会导致误报，如在123个真实程序中出现了44%的误报率。
- 提出了一种基于硬件精准的验证方法，该方法利用声明式HAL描述符和健全的降低策略，以目标宽度解释算术运算，并将输入约束在硬件可实现范围内。
- 该方法以ArduinoTool形式实现，在保持鲁棒性证明的同时消除了所有误报，并能通过可实现的反例检测罕见的宽度相关缺陷。