ESBMC-Arduino：缩小开放式硬件PLC形式验证的部署差距

摘要

该论文揭示了现有IEC 61131-3形式验证工具在资源受限微控制器上的部署差距，即忽略硬件输入模型会导致大量误报。作者提出了硬件忠实验证方法，通过模拟有限分辨率ADC和16位字长，解决了传感器值范围不匹配的问题，并实现了对真实缺陷的检测。