解决图形化PLC程序形式化验证难题，让工具能正确理解梯形图逻辑。
ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking
- 基于深度优先搜索解析梯形图连接图，提取触点逻辑路径。
- 3个图形化程序在70ms内验证通过，且生成完整中间表示。
- 适合工业控制安全验证人员，尤其关注PLCopen图形代码的开发者。
PLCopen XML定义了IEC 61131-3梯形图程序的两种编码格式：文本格式使用<rung>元素，图形格式则以localId/refLocalId连接构成有向图。现有ESBMC-PLC仅支持文本格式，将CONTROLLINO、Beremiz和OpenPLC Editor的图形导出解析为空GOTO中间表示，导致虚假验证成功。本文提出ESBMC-GraphPLC，采用基于深度优先搜索的图形化梯形图解析器，从左电源轨出发遍历至每个线圈，提取触点合取式作为运行逻辑，并引入三层输入/输出推断机制。通过按右电源轨连接点顺序排列线圈，确保置位（SET）线圈先于复位（RESET）线圈处理，符合IEC扫描周期语义。图形到中间表示的转换保持ESBMC后端不变。对来自CONTROLLINO/OpenPLC Editor的3个图形梯形图程序进行验证，均生成包含非确定性输入与运行逻辑的完整GOTO IR，而此前为无内容表示；所有3个在k=2下验证为SAFE，耗时小于70ms。11个文本梯形图基准测试完全保留，无退化现象。两个Beremiz示例因无梯形图内容或不支持定时器语义被报告为局限。代码与数据存于Zenodo（DantasCordeiro2026graphical, doi:10.5281/zenodo.20699856）。
原文摘要 · Abstract (English)
PLCopen XML defines two encoding formats for IEC 61131-3 Ladder Diagram programs: a textual encoding using <rung> elements, and a graphical encoding that represents rung logic as a directed graph of localId/refLocalId connections. ESBMC-PLC supported the textual format but parsed graphical exports from CONTROLLINO, Beremiz, and OpenPLC Editor into an empty GOTO intermediate representation, causing vacuous verification success. This paper presents ESBMC-GraphPLC, which closes this gap with a DFS-based graphical LD resolver. The resolver traverses the connection graph from leftPowerRail to each coil, extracts rung paths as Boolean contact conjunctions, and applies a three-tier I/O inference scheme. Ordering coils by rightPowerRail connectionPointIn sequence ensures SET coils process before RESET coils, matching IEC scan-cycle semantics. The graphical-to-IR conversion leaves the ESBMC backend unchanged. Validation on 3 graphical LD programs from CONTROLLINO/OpenPLC Editor shows all produce full GOTO IR with nondeterministic inputs and rung logic, versus the empty IR previously. All 3 verify SAFE at k=2 under 70ms. The 11 textual LD benchmarks are fully preserved, with no regression. Two Beremiz examples with no LD content or unsupported timer semantics are reported as discovered limitations. Artifact at Zenodo (DantasCordeiro2026graphical, doi:10.5281/zenodo.20699856).
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。