首个支持梯形图的开源形式化验证工具，可自动检测工业PLC程序缺陷。
ESBMC-PLC: Formal Verification of IEC 61131-3 Ladder Diagram Programs Using SMT-Based Model Checking
- 将梯形图转换为GOTO中间表示，用SMT求解器验证安全属性。
- 在13个基准上正确识别61项性质，发现8个真实缺陷，全部分析<60ms。
- 适合工业自动化开发者和安全验证研究人员使用。
PLC在工业领域执行安全关键程序。主流的梯形图（LD）编程语言（IEC 61131-3标准）长期缺乏形式化验证支持，因SMT模型检测器无法处理其梯形结构。本文提出ESBMC-PLC，首个原生支持梯形图（PLCopen XML格式）的开源形式化验证工具，作为ESBMC的新前端实现。该工具将梯形图语句转换为GOTO中间表示，将PLC扫描周期建模为含非确定输入的while(true)循环，通过基于SMT的有界模型检测或k-归纳法验证安全性质。采用五类性质的YAML语言（互斥、不变性、不存在、响应、可达性），避免使用时序逻辑。对22项研究（2020–2026）的调研揭示四个研究空白，ESBMC-PLC填补其中两个。在13个基准测试中（6个领域，3个来源——包括实际部署的CONTROLLINO PLC与MathWorks Simulink PLC Coder生成代码），成功分类61项性质：所有9个作者构造程序（类别A/B）结果正确，4个厂商程序（类别C）均被准确标注，共发现8个缺陷（提供可操作反例），7个未受限制的k-归纳证明，所有运行时间均低于60毫秒（苹果硅芯片）。与PLCverif的功能对比显示，ESBMC-PLC是唯一同时具备原生梯形图支持、k-归纳和SMT位向量语义的开源工具。
原文摘要 · Abstract (English)
PLCs execute safety-critical programs across industrial sectors. The dominant PLC notation, ladder diagram (LD) per IEC 61131-3, remains absent from formal verification: SMT-based model checkers cannot process LD's rung-and-coil graphics. This paper presents ESBMC-PLC, the first open-source formal verifier with native LD support (PLCopen XML format), implemented as a new ESBMC frontend. ESBMC-PLC translates LD rungs to GOTO IR, models the PLC scan cycle as a while(true) loop with nondeterministic inputs, and checks safety properties via SMT-based bounded model checking or k-induction. A five-property YAML language (mutual_exclusion, invariant, absence, response, reachability) avoids temporal logic. A survey of 22 studies (2020-2026) identifies four research gaps; ESBMC-PLC closes two of them. Evaluation on 13 benchmarks (6 domains, 3 sources - including deployed CONTROLLINO PLCs and MathWorks Simulink PLC Coder) shows correct classification across 61 properties: all 9 author-constructed programs (Categories A/B) as expected, all 4 vendor programs (Category C) correctly unlabeled, with 8 bugs found (actionable counterexamples), 7 unbounded k-induction proofs, all runs under 60ms on Apple Silicon. Feature comparison with PLCverif shows that ESBMC-PLC is the only open-source tool that combines native LD, k-induction, and SMT bit-vector semantics.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。