查看 PDF HTML（实验性） 摘要：OpenPLC、Arduino OPTA、CONTROLLINO 和工业盾 M-Duino 将 IEC 61131-3 引入用于真实自动化和工业控制系统（ICS）安全研究的低成本微控制器。现有的用于 IEC 61131-3 的开源验证工具，包括 ESBMC-PLC，在理想化的无界整数反抽象扫描周期模型上验证安全性。该板件在资源受限的微控制器单元（MCU）上运行，字长为 16 位（8 位 AVR Arduino），并通过有限分辨率的模拟到数字转换器（ADC）读取传感器。我们展示了这一部署差距使得简单的宽度感知验证不可靠：在 123 个真实程序中，检查 16 位溢出而不使用硬件输入模型导致 44% 的误报（54/123），并发现没有真正的缺陷，因为它探测的传感器值是任何 ADC 无法产生的。由于这个差距出现在计算与物理过程交汇的地方——一个被有限宽度算术缩放的有界传感器读取，转化为控制命令——因此溢出可能在不知不觉中抑制安全行为，例如高级警报。一个无界输入模型制造出环境无法触发的警报。我们为开放硬件的 IEC 61131-3 提出了符合硬件的验证：一个声明式硬件抽象层（HAL）描述符（宽度、ADC/PWM 分辨率、I/O 绑定）以及一个合理的降低，按目标宽度解释算术并将输入限制为可实现的硬件范围。我们为 Arduino 实现了 ArduinoTool，从官方核心中推导 HAL 参数，并在 ESBMC 梯形图（LD）前端实现输入范围模型。在 123 个程序组合中，HAL 注释器消除了所有 54 个误报，同时保留了鲁棒性证明，并且一个受控组合展示了它检测到的稀有宽度相关缺陷以及可实现的证据。评论：21 页 主题：编程语言（cs.PL）；硬件架构（cs.AR）；系统与控制（eess.SY） 引用为：arXiv:2607.08550 [cs.PL]（或 arXiv:2607.08550v1 [cs.PL] 对于此版本） https://doi.org/10.48550/arXiv.2607.08550 arXiv 发布的 DOI 通过 DataCite 提交历史 作者：Pierre Dantas [查看电子邮件] [v1] 2026 年 7 月 9 日 14:42:15 UTC（44 KB）