ESBMC-PLC：基于 SMT 模型检查的 IEC 61131-3 梯形图程序形式化验证

背景

可编程逻辑控制器（PLC）广泛应用于各个工业领域，负责执行涉及安全的关键程序。在这些程序中，梯形图（Ladder Diagram, LD）是依据 IEC 61131-3 标准主导的编程表示法。然而，梯形图在形式化验证领域长期处于空白状态。现有的基于 SMT（可满足性模理论）的模型检查器无法直接处理梯形图中特有的“梯级-线圈”（rung-and-coil）图形化结构，导致难以对这类工业核心代码进行严格的数学证明和错误检测。这一技术缺口使得工业界在确保 PLC 程序安全性时，往往依赖于传统的测试方法，而非形式化的数学验证。

核心内容

本文介绍了 ESBMC-PLC，这是首个原生支持梯形图（LD）形式化验证的开源工具。该工具作为 ESBMC（Efficient SMT-Based Model Checker）的一个新前端实现，专门针对 PLCopen XML 格式的梯形图程序进行了优化。

技术实现机制

ESBMC-PLC 的核心工作流程包括以下几个关键步骤：

1. 语法转换：将梯形图的梯级（rungs）转换为 GOTO 中间表示（IR）。
2. 扫描周期建模：将 PLC 的扫描周期建模为一个 while(true) 循环，其中包含非确定性输入（nondeterministic inputs），以模拟真实工业环境中的输入变化。
3. 安全性检查：利用基于 SMT 的有界模型检查（Bounded Model Checking, BMC）或 k-归纳法（k-induction）来验证安全性属性。

验证语言与属性

为了避免使用复杂的时序逻辑（Temporal Logic），ESBMC-PLC 采用了一种简化的五属性 YAML 语言来定义验证目标。这五种属性包括：

• 互斥性（Mutual Exclusion）
• 不变性（Invariant）
• 无错误性（Absence）
• 响应性（Response）
• 可达性（Reachability）

研究现状与差距

通过对 2020 年至 2026 年间发表的 22 项相关研究进行综述，作者识别出当前领域存在的四个主要研究空白。ESBMC-PLC 的提出填补了其中两个关键空白。

评估结果

研究团队在 13 个基准测试集上对 ESBMC-PLC 进行了评估，涵盖了 6 个不同领域和 3 个不同来源（包括已部署的 CONTROLLINO PLC 和 MathWorks Simulink PLC Coder 生成的代码）。评估结果如下：

• 正确分类：在 61 个属性验证中实现了完全正确的分类。
• 作者构建程序：所有 9 个作者构建的程序（类别 A/B）均按预期通过验证。
• 厂商程序：所有 4 个厂商提供的程序（类别 C）均被正确标记为未通过（unlabeled，此处指未通过验证或发现潜在问题，结合上下文“correctly unlabeled”及后续发现 bug，意指准确识别出风险）。
• 缺陷发现：共发现 8 个 bug，并提供了可操作的反例（counterexamples）。
• 证明能力：成功完成了 7 个无界 k-归纳证明。
• 性能表现：所有运行均在 Apple Silicon 芯片上于 60 毫秒内完成。

工具对比

与 PLCverif 等其他工具的功能对比显示，ESBMC-PLC 是目前唯一一款同时具备原生梯形图支持、k-归纳法验证能力以及 SMT 位向量语义（bit-vector semantics）的开源工具。

关键要点

• 首创性：ESBMC-PLC 是首个原生支持 IEC 61131-3 梯形图（PLCopen XML 格式）的开源形式化验证器。
• 技术路径：通过梯形图到 GOTO IR 的转换，结合 while(true) 循环模拟 PLC 扫描周期，利用 SMT 求解器进行有界模型检查或 k-归纳验证。
• 简化验证语言：摒弃复杂的时序逻辑，采用包含互斥性、不变性、无错误性、响应性和可达性的五属性 YAML 语言。
• 高性能与高精度：在 Apple Silicon 平台上，所有验证运行时间均低于 60 毫秒；在 13 个基准测试的 61 个属性中实现 100% 正确分类。
• 独特优势：区别于其他工具，ESBMC-PLC 是唯一结合原生 LD 支持、k-归纳法和 SMT 位向量语义的开源解决方案。
• 实际效用：能够发现实际部署系统中的 bug（如 CONTROLLINO 和 Simulink Coder 生成的代码），并提供可操作的错误反例。

意义与影响

ESBMC-PLC 的发布填补了工业控制软件形式化验证领域的一项重要空白。梯形图作为工业自动化中最主流的编程方式，长期以来缺乏有效的数学验证手段，导致潜在的安全隐患难以通过形式化方法提前发现。ESBMC-PLC 通过引入 SMT 模型检查技术，使得工程师能够以极高的效率（毫秒级）和严谨性对 PLC 代码进行安全性证明。

该工具不仅提升了 PLC 程序开发的安全标准，还为工业 4.0 背景下的软件可靠性提供了新的技术路径。其开源特性及与现有工业工具链（如 Simulink）的兼容性，有望推动形式化验证技术在更广泛的工业场景中的落地应用，特别是在对安全性要求极高的关键基础设施领域。此外，通过填补现有研究中的两个关键空白，ESBMC-PLC 也为后续关于 PLC 形式化验证的研究奠定了新的基准。