AI 中文总结
研究IEC 6113-梯形图验证器翻译问题，核心方法是构建K-ESBMC可执行形式语义，主要贡献是为审核验证器翻译提供标准忠实预言机，验证翻译工具健全性，提升正确性论证从经验到形式。
AI 中文摘要
IEC 61131-3梯形图的自动验证器通过将梯形图转换为模型检查器输入来提高安全性。然而，其未经验证的前端翻译在与标准不一致时可能会默默地返回错误结果。我们使用K-ESBMC来解决这一差距，它是在K框架中构建的IEC 61131-3梯形图的可执行形式语义。K-ESBMC对触点、线圈、定时器、计数器、边缘块和保持扫描周期进行建模，从单一定义生成解释器和演绎验证器。与OpenPLC/Matiec逐扫描验证，K-ESBMC作为独立参考预言机来差异测试ESBMC可编程逻辑控制器（PLC）梯形图到GOTO的转换。它与ESBMC在大多数程序上一致，并通过具体见证重现注入的违规情况。每一处不一致都暴露了ESBMC的真正缺陷，经OpenPLC和其他两个验证器确认，揭示了两种失败模式。对于组合和锁存片段，我们在kprove中机器检查Kes BMC的规则实现了标准的输入/输出关系，将正确性论证从经验提升到形式。K-ESBMC为审核任何梯形图验证器的翻译提供了一个可重用、忠实于标准的预言机，为验证基于翻译的验证工具的健全性提供了一种通用方法。
英文摘要
Automated verifiers for IEC 61131-3 ladder diagrams enhance safety by translating diagrams into model-checker inputs. Still, their unverified front-end translations risk silently returning incorrect results (missing violations or raising false alarms) when they diverge from the standard. We address this gap with K-ESBMC, an executable formal semantics of IEC 61131-3 ladder diagrams built in the K framework. K-ESBMC models contacts, coils, timers, counters, edge blocks, and the retentive scan cycle, generating both an interpreter and a deductive verifier from a single definition. Validated scan-for-scan against OpenPLC/Matiec, K-ESBMC serves as an independent reference oracle to test the ESBMC Programmable Logic Controller (PLC) ladder diagram to GOTO translation differentially. It agrees with ESBMC on most programs and reproduces injected violations with concrete witnesses. Every disagreement exposes a genuine ESBMC defect, confirmed by OpenPLC and two other verifiers, revealing two failure modes: an unsound skip that certifies unsafe programs, and an imprecise havoc that produces spurious counterexamples. For the combinational and latch fragment, we machine-check in kprove that Kes BMC's rules implement the standard's input/output relation, elevating the correctness argument from empirical to formal. K-ESBMC provides a reusable, standard-faithful oracle for auditing any ladder diagram verifier's translation, offering a general approach to verifying the soundness of translation-based verification tools.
Comments19 pages
