发表机构
University of Manchester; Federal University of Amazonas (UFAM)（曼彻斯特大学; 亚马孙联邦大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对PLC程序形式化验证缺乏标准基准的问题，提出首个结合受控真值与ST/LD编码覆盖的基准套件，含50程序83变体，通过三方真值纪律和跨工具验证确保可靠性，并发布开放工件。
AI 中文摘要
我们提出了首个用于可编程逻辑控制器（PLC）程序形式化验证的基准测试套件，该套件将受控真值与对文本（结构化文本，ST）和图形（梯形图，LD）IEC 61131-3 编码的覆盖相结合。尽管对工具的支持日益增长，但该领域缺乏标准评估基准：现有语料库省略了形式化属性或图形方言，私有程序集阻碍了可复现的进展测量。我们的套件包含跨越十个工业领域的 50 个程序的 83 个变体，以 PLCopen 可扩展标记语言（XML）和 ST 提供，每个程序都配有一个形式化属性、机器可检查的预期判定结果，以及符合软件验证竞赛（SV-COMP）格式的违规见证。核心方法论贡献是一种三方真值纪律——判定结果通过构造、故障注入或审计的跨工具共识建立——其动机是一个具体的失败模式，即明显的安全属性错误地将来自两个公共逻辑炸弹语料库的所有攻击归类为安全，原因是不可见的非终止。参考判定结果使用基于 SMT 的高效上下文有界模型检查器（ESBMC）v8.4 从源代码获得：所有 25 个图形基准均可执行，45 个接受变体中的 43 个与记录的判定结果匹配。在有限状态片段（21 个基准）上，nuXmv——一个具有不相关决策过程的模型检查器——在所有 24 个互锁变体上达成一致，并解决了 ESBMC-PLC 留作未知的两个基准，确认了工具无关的真值和判别能力。移植暴露了格式和语义碎片化：前端接受不同的序列化，定时器语义因工具而异——这些现象正是该套件旨在揭示的。语料库、模式、验证器和重新检查工具链作为开放工件发布。
英文摘要
We present the first benchmark suite for formal verification of Programmable Logic Controller (PLC) programs that combines controlled ground truth with coverage of both textual (Structured Text, ST) and graphical (Ladder Diagram, LD) IEC 61131-3 encodings. Despite growing support for tools, the field lacks standard evaluation benchmarks: existing corpora omit formal properties or graphical dialects, and private program sets preclude reproducible measurement of progress. Our suite comprises 50 programs in 83 variants across ten industrial domains, provided in PLCopen Extensible Markup Language (XML) and ST, each paired with a formal property, machine-checkable expected verdict, and violation witness in the Software Verification Competition (SV-COMP) format. The central methodological contribution is a tripartite ground-truth discipline - verdicts are established by construction, fault injection, or audited cross-tool consensus - motivated by a concrete failure mode where the obvious safety property misclassifies all attacks from two public logic-bomb corpora as safe due to invisible non-termination. Reference verdicts are obtained with the Efficient SMT-Based Context-Bounded Model Checker (ESBMC) v8.4 from source: all 25 graphical benchmarks execute, and 43 of 45 accepted variants match recorded verdicts. On the finite-state fragment (21 benchmarks), nuXmv - a model checker with unrelated decision procedures - agrees on all 24 interlock variants and resolves two benchmarks ESBMC-PLC leaves unknown, confirming tool-neutral ground truth and discriminative power. Porting exposes format and semantics fragmentation: front-ends accept different serializations, and timer semantics vary across tools - phenomena the suite is designed to reveal. The corpus, schema, validator, and recheck harness are released as open artifacts.
Comments11 pages
