ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking
本文介绍了 ESBMC-GraphPLC，这是一种形式化验证工具，它通过实现一种基于深度优先搜索（DFS）的解析器，将基于图的梯形图逻辑转换为有效的 GOTO 中间表示，从而解决了处理图形化 PLCopen XML 梯形图方面的空白，进而实现了对来自 CONTROLLINO 和 OpenPLC Editor 等编辑器的程序的正确验证，且不影响现有的文本格式支持。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，将可编程逻辑控制器（PLC）视为工厂机器（如水泵或红绿灯）的大脑。为了告诉这个大脑该做什么，工程师会绘制梯形图（Ladder Diagrams）。这些图看起来像带有横档的电气梯子，每个横档都是一条规则：“如果水箱满了，就关闭水泵。”
长期以来，有两种方法可以将这些梯形图图纸保存在计算机中：
- 文本列表（The Text List）： 一个简单的、逐步进行的指令列表（就像食谱一样）。
- 图形映射（The Graphical Map）： 一个视觉化的地图，其中的组件通过 ID 数字进行连接（就像车站由线路连接起来的地铁图）。
问题所在：“幽灵”程序
研究人员拥有一种强大的工具叫做 ESBMC-PLC，它可以检查这些程序的安全性错误。它在处理文本列表格式时表现得非常完美。
然而，当他们将图形映射格式（这是 CONTROLLINO 和 OpenPLC 等现代软件实际使用的格式）输入给工具时，工具却产生了困惑。它看到了地图、ID 数字和导线，但无法理解它们是如何连接的。
- 结果： 工具显示：“一切都是安全的！”
- 陷阱： 它在撒谎。它之所以认为“安全”，并不是因为逻辑正确，而是因为工具面对的是一个空荡荡的房间。这被称为空虚验证（vacuous verification）——这就像是因为你忘了检查窗户是否开着，就断言一扇锁着的门是绝对安全的。
解决方案：ESBMC-GraphPLC
作者构建了一个名为 ESBMC-GraphPLC 的新模块来解决这个问题。你可以把它想象成雇佣了一名侦探，让其穿梭于图形映射之中，并将其翻译回安全检查器能够理解的语言。
以下是他们的“侦探”的工作方式，使用了简单的类比：
1. 带着手电筒的侦探（DFS 算法）
该工具使用了一种称为**深度优先搜索（DFS）**的方法。想象一名侦探正在走过一个布满电线的迷宫。他们从梯子的左侧（电源端）开始，沿着每一条可能的路径走到右侧。
- 他们追踪每一条导线连接。
- 他们记录下经过的每一个开关（触点）。
- 当他们到达设备（线圈/泵）时停止。
- 通过这样做，他们重建了梯形图横档的确切逻辑，将视觉地图转回清晰的“如果-那么（If-Then）”规则。
2. 交警（顺序至关重要）
在这些图中，有时同一个设备会同时拥有一个“置位（Set）”开关（开启）和一个“复位（Reset）”开关（关闭）。顺序非常重要！
- 如果“复位”发生在同一瞬间的“置位”之后，“复位”生效，设备保持关闭。
- 如果“置位”发生在“复位”之后，“置位”生效，设备保持开启。
这个新工具会查看文件中的一个特定列表（rightPowerRail序列），以观察哪个开关先出现，就像一名交警确保“置位”车在“复位”车之前通过一样。这确保了逻辑符合真实机器的行为方式。
3. 猜谜游戏（I/O 推断）
有时地图并不会说明哪些导线是“输入”（传感器）以及哪些是“输出”（电机）。该工具使用了一个三步走的猜谜游戏：
- 第一步： 寻找官方地址标签（例如用于输入的
%IX）。如果找到了，则是精确的。 - 第二步： 如果没有标签，则观察行为。如果一根导线仅被用作开关，它很可能是一个输入；如果它仅被用于开启某物，它很可能是一个输出。
- 第三步： 如果仍不确定，则将其视为一个“神秘变量”，它可以是任何东西。这是一个稳妥的做法，因为它检查了所有可能性，确保没有任何遗漏。
结果
团队在三个现实世界的程序（水泵、楼梯灯和调光灯）上测试了这个新侦探。
- 之前： 工具看到的是一个空房间，并说“安全”（错误判断）。
- 之后： 工具看到了完整的逻辑，检查了所有可能的传感器输入组合，并确认了程序确实是安全的。
- 速度： 它完成这一切用了不到 70 毫秒（比人类眨眼还快）。
- 安全性： 它没有破坏旧有的工具。原本在文本列表下运行良好的 11 个程序依然可以完美运行。
目前还做不到的事情（局限性）
论文诚实地说明了这位侦探目前仍在挣扎的地方：
- 复杂的定时器： 如果一个横档涉及定时器（例如，“等待 5 秒，然后打开”），该工具目前会忽略“等待”部分，并将其视为随机猜测。这虽然保证了安全性，但它并不理解时间逻辑。
- 嵌套地图： 一些复杂的图表会将更小的地图隐藏在其他部分内（例如，步骤中的动作）。侦探有时会错过这些隐藏的房间。
总结
简而言之，作者构建了一个翻译器，使安全检查软件终于能够“阅读”现代工业软件所使用的视觉梯形图。他们将一个只会盲目说“一切正常”的工具，变成了一个真正理解逻辑并能证明机器不会损坏或伤人的工具。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。