A Benchmark Suite and Ground-Truth Methodology for Formal Verification of IEC 61131-3 Ladder Diagram Programs

RESUMO

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.