ESBMC-PLC: Formal Verification of IEC 61131-3 Ladder Diagram Programs Using SMT-Based Model Checking
本文介绍了 ESBMC-PLC，这是首个通过将 IEC 61131-3 梯形图程序转换为用于基于 SMT 的模型检测的中间表示，从而原生支持该程序的开源形式化验证器，它在成功验证安全属性并检测各类工业基准测试中的缺陷的同时，解决了该领域关键的研究空白。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一个工厂车间，巨大的机器、化学混合器和火车信号灯都由一个被称为 PLC（可编程逻辑控制器）的微小且不知疲倦的大脑控制着。这些机器运行在一套特殊的指令手册上，叫做 梯形图（Ladder Diagram）。你可以把它想象成一张梯子的图纸，每一“横档”都是一条规则：“如果红灯亮起 且 按键被按下，那么启动电机。”
几十年来，工程师们一直通过绘图而非编写代码来编写这些规则。这使得现代“安全检查员”（形式化验证工具）很难检查这些规则是否完美，因为检查员只理解文本代码，而不理解图形。
这篇论文介绍了一个名为 ESBMC-PLC 的新工具，它既是一个通用翻译官，也是一个极其严格的安全检查员。
以下是它的工作原理，使用了简单的类比：
1. 翻译官（“罗塞塔石碑”）
在此工具出现之前，你无法要求计算机检查一张图纸。ESBMC-PLC 将图形化的“梯形图”（绘图）瞬间转化为计算机能够理解的语言（基于文本的中介代码）。
- 类比： 想象你有一份用素描本记录的食谱，上面画着食材的图片。ESBMC-PLC 就像一位大厨，他看着图片，能立刻写出精确的文字指令：“加入 2 杯面粉，然后搅拌。”现在，计算机可以阅读这份食谱了。
2. 模拟器（“时空循环”）
PLC 不仅仅运行一次；它在一个循环中运行，每秒钟检查传感器并改变输出数千次。
- 类比： 大多数安全检查只观察单一的时间点。ESBMC-PLC 则像是一个时空旅行模拟器，它一遍又一遍地模拟工厂的“每一天”。但它不仅仅是在重放某一个特定的日子，而是在同时模拟所有可能的日子。它会追问：“如果传感器坏了怎么办？如果按键被按了两次怎么办？如果电源闪烁了怎么办？”它会检查所有可能的事件组合，以查看是否会出现灾难。
3. “无界”证明（“永恒保证”）
旧有的工具只能检查有限的步骤（比如检查工厂诞生的前 100 天）。如果 Bug 出现在第 101 天，它们就会漏掉。
- 类比： ESBMC-PLC 使用了一种称为 k-归纳法（k-induction）的特殊数学技巧。它不是一天一天地计数，而是证明一条规则，即：“如果工厂今天是安全的，且规则被遵守了，那么明天、后天以及永远都是安全的。”它提供了一个永恒的保证，确保只要规则被遵守，机器就永远不会崩溃。
4. “非逻辑”语言（“白话文”清单）
通常，要让计算机进行安全检查，你需要掌握复杂的数学逻辑（时序逻辑）。
- 类比： ESBMC-PLC 让工程师可以使用简单的 YAML 清单（就像一份待办事项列表）来编写安全规则。
- 与其说： “对于所有时间 t，如果 A 为真，则 B 必须为假。”
- 你只需写： “电机和反转开关绝不能同时开启。”
该工具能理解这种直白的语言，并自动进行检查。
他们发现了什么？
作者在 13 个不同的工厂程序上测试了这个工具，涵盖了从简单的电机控制到复杂的交通灯和水泵。他们使用的程序来自真实的供应商（如 CONTROLLINO 和 MathWorks），这些程序原本并非为了接受测试而设计，仅用于测试该工具的处理能力。
- 结果：
- 100% 的准确率： 它正确识别了每一个安全的程序和每一个不安全的程序。
- 发现了隐藏的 Bug： 它发现了 8 个标准测试未能发现的具体 Bug。例如，它发现了一种情况：紧急停止按钮虽然关闭了机器，但却未能复位计时器，导致在按下按钮释放后，机器会立即重新启动。
- 速度： 它检查所有这些程序的时间不到 60 毫秒（比人类眨眼还要快）。
核心结论
这篇论文展示了第一个能够获取标准工业绘图（梯形图）、对其进行翻译并从数学上证明其永久安全的开源工具。它弥合了工程师设计机器的传统图形化方式与计算机验证安全的高科技数学方式之间的鸿沟。
重要提示： 论文声称，这适用于工业编程的特定“核心”部分（布尔逻辑、定时器、计数器）。它目前还无法处理复杂的特性，如浮点数或高级数据数组，但对于绝大多数对安全性至关重要的逻辑，它运行完美，并且已经可以投入使用。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。