Source-linked AI summary
A Benchmark Suite and Ground-Truth Methodology for Formal Verification of IEC 61131-3 Ladder Diagram Programs
Pierre Dantas, Lucas Cordeiro, Waldir Junior
TL;DR
PLC verification lacks a standard benchmark with formal properties and expected verdicts, while the property-bearing suite identified by the authors covers ST only. The suite pairs programs with formal properties, machine-checkable verdicts, and violation witnesses, establishing labels by construction, fault injection, or audited cross-tool consensus. ESBMC-PLC ran all 25 graphical PLCopen XML benchmarks; 43 of 45 accepted variants matched ground truth, and nuXmv agreed with ESBMC-PLC on all 24 variants and resolved two edge-detector UNKNOWNs.
Problem
PLC verification lacks a standard benchmark with formal properties and expected verdicts, while the property-bearing suite identified by the authors covers ST only.
Source: §1 · p. 2Method
Results
ESBMC-PLC ran all 25 graphical PLCopen XML benchmarks; 43 of 45 accepted variants matched ground truth, and nuXmv agreed with ESBMC-PLC on all 24 variants and resolved two edge-detector UNKNOWNs.
Source: §6.1 · p. 7, §6.3 · p. 7Takeaways & Limitations
The suite provides a shared evaluation target, and its tool comparisons make input-format and scan-cycle semantics fragmentation measurable.
Source: §6.4 · p. 8, §8 · p. 9The multi-tool comparison covers only finite-state graphical benchmarks; non-termination, textual-LD, and ST benchmarks remain single-tool, and a complete multi-tool matrix remains future work.
Source: §6.4 · p. 8
Abstract
from arXiv · showhide
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.
1 Introduction
PLC verification lacks a shared benchmark with formal properties and trusted verdicts, limiting comparable evaluation. This paper introduces a cross-language suite with an explicit ground-truth methodology and reproducible artifacts.
1 Introduction
- Without a standard benchmark, PLC verification claims of coverage, precision, and extensibility cannot be compared, and no shared target exists for demonstrating improvement.Existing corpora lack formal properties or expected verdicts, while the property-bearing suite described in the paper covers ST only.Source: §1 · p. 2
- The suite contains 50 benchmarks across 83 variants, covering textual and graphical LD and ST in ten industrial fields, with properties, expected verdicts, and violation witnesses.Its SV-COMP-compatible layout, schema validator, and recheck harness support adding tools through adapters.Source: §1 · p. 2, Contributions · p. 2
- Verdicts are established by construction, fault injection, or audited cross-tool consensus; logic-bomb variants show why assuming the intended safety property can mislabel attacks.The injected non-terminating loops leave valve logic untouched, making scan-cycle termination the distinguishing property.Source: §1 · p. 2
Contributions
- ESBMC-PLC verifies all 25 graphical benchmarks, with 43 of 45 accepted variants matching ground truth; nuXmv agrees on all 24 interlock variants and resolves two unknowns.These baseline results are reported as evidence of tool-neutral ground truth and the suite's ability to discriminate between tools.Source: Contributions · p. 2
- The corpus, property files, witnesses, schema, validator, and recheck harness are archived under a citable DOI at the baseline tool commit.Source: Contributions · p. 2
2 Related Work
Prior PLC verification tools use private or incomparable program sets, while existing corpora and semantics work serve different purposes. The paper positions its suite as a shared, verdict-bearing evaluation target spanning graphical LD and other IEC 61131-3 forms.
2.1 Formal Verification of IEC 61131-3
- PLC verification tools have been evaluated on private or incomparable program sets with ad hoc properties, preventing cross-tool claims from being checked.The suite is complementary to those tools: it provides a common target and evaluates several of them on it.Source: §2.1 · p. 3
2.2 Benchmark Suites and Verification Competitions
- The closest prior property-bearing PLC suite covers ST only; this suite adds graphical LD coverage and records ground-truth provenance for every task.The paper adapts the SV-COMP and Test-Comp task model, adding PLC-specific coverage and verdict practices.Source: §2.2 · p. 3
2.3 PLC Program Corpora and ICS Security Datasets
- PLC-LD, SWaT, and PPU corpora provide programs but no formal properties or expected verdicts; the suite converts reused programs into verification tasks with triangulated labels.The malicious label alone does not identify which formal property is violated.Source: §2.3 · p. 3
2.4 Formal Semantics of IEC 61131-3
- Prior formal-semantics work targets IEC 61131-3 language meaning, whereas this paper targets a shared corpus for evaluating verification tools.The suite's feature micro-benchmarks draw on an independent executable LD-semantics effort, supporting tool-independent verdicts.Source: §2.4 · p. 3
3 Design Principles
The design principles prioritize trustworthy, machine-checkable verdicts and explicit properties, while balancing language, domain, and difficulty coverage with realistic provenance, tool discrimination, and reproducibility.
3 Design Principles
- Every task pairs a program with a formal property, and each machine-checkable verdict is established by construction, fault injection, or audited cross-tool consensus.The paper treats the verdict as the primary artifact and excludes tasks when realism or coverage would require an unverifiable verdict.Source: §3 · pp. 3–4
- The suite spans textual LD, graphical LD, and ST across ten industrial sectors, with difficulty ranging from feature micro-benchmarks to multi-PLC controllers.Graphical LD receives deliberate emphasis because real programs are exchanged in that encoding and prior suites do not target it.Source: §3 · p. 4
- Expected verdicts are balanced roughly between SAFE and VIOLATION, with a hard tier retained so the suite can expose unknown outcomes and distinguish tools.This also requires tools to demonstrate both proof and refutation rather than succeed by always answering “safe.”Source: §3 · p. 4
- The suite prefers third-party programs where available and authors programs to fill genuine domain or construct gaps, disclosing the split to help readers weigh realism against control.Authored programs use standard control idioms rather than tool-specific patterns.Source: §3 · p. 4
- A schema-validated SV-COMP-aligned format and one-command harness let tools run through adapters and recheck verdicts, while recording programs a tool cannot ingest.The format is intended to let the suite seed an SV-COMP PLC/ICS category directly.Source: §3 · p. 4
4 The Benchmark Suite
The suite combines validated, machine-readable verification tasks with coverage across languages, domains, provenance, property types, and equivalent syntax variants.
4 The Benchmark Suite
- Each benchmark is a schema-validated verification task pairing an IEC 61131-3 program with a machine-checkable property and expected verdict in an SV-COMP-compatible layout.The task runner dispatches programs through tool adapters, including translation where a tool does not ingest PLCopen XML natively.Source: §4 · p. 4, Figure 1 · p. 5
4.1 Composition
- The 50-benchmark suite includes 15 textual LD, 25 graphical LD, and 10 ST benchmarks across ten industrial fields, deliberately emphasizing graphical LD.Water treatment is the largest domain because the two richest public ICS corpora used are in that domain.Source: §4.1 · p. 4, Table 1 · p. 5
4.2 Provenance
- Nineteen benchmarks come from third-party or prior corpora, while 31 authored benchmarks fill construct and domain gaps.The authored set includes feature micro-benchmarks and domain control programs, including domains without public programs.Source: §4.2 · pp. 4–5
4.3 Properties and coverage
- The suite covers invariant, termination, mutual-exclusion, and reachability properties; scan-cycle termination addresses logic bombs based on non-terminating loops.The stated property counts are 29 invariant, 14 termination, 6 mutual_exclusion, and 3 reachability properties.Source: §4.3 · p. 5
4.4 Syntax-coverage pairs
- Five graphical-LD renderings preserve the logic of textual-LD or ST originals, enabling differential checks of whether tools return the same verdict across encodings.These syntax pairs are explicitly flagged and counted once for each language slice.Source: §4.4 · p. 6
5 Ground-Truth Methodology
The methodology establishes verdicts by construction, fault injection, or audited agreement between independent tools. It treats code inspection as essential when an intuitive safety property misses a seeded non-termination defect.
Ground-truth overview
- Across 83 variants, the three grounding methods account for 36, 29, and 18 variants, alongside 49 SAFE and 34 VIOLATION verdicts.The method used for each variant is recorded in its benchmark descriptor.Source: §5 · p. 6
Construction
- Feature micro-benchmarks and authored domain interlocks receive EXPERT verdicts based on inspection of their properties.Examples include mutually exclusive outputs under a series interlock and a not-full contact guarding a fill-valve rung.Source: §5 · p. 6
Fault injection
- 29 VIOLATION variants are documented mutants of known-safe bases, with seeded defects and triggering witnesses; both public corpora supply fault-injected malicious siblings.Inspection found that the malicious siblings preserve functional logic but contain non-terminating loops, so termination—not valve safety—distinguishes them.Source: §5 · p. 6
Audited cross-tool consensus
- For SAFE variants without a by-construction verdict, independent-tool agreement is required, and disagreements are manually audited and reported.Programs on which mature tools disagree are retained as informative benchmarks.Source: §5 · p. 6
Rechecking
- The recheck harness runs every variant with mode-specific verification and a scan watchdog, then compares outcomes with recorded verdicts in a pass/fail table.It uses k-induction for expected-SAFE tasks and incremental BMC for expected-VIOLATION tasks; the harness and suite are archived with a citable DOI.Source: §5 · pp. 6–7
6 Evaluation
The evaluation checks the suite with ESBMC-PLC and independently compares finite-state cases with nuXmv. Results show strong agreement on accepted graphical variants, while format and semantics differences constrain tool coverage and cross-tool scope.
6 Evaluation
- ESBMC-PLC was built from source with its LD frontend enabled; expected-SAFE tasks used k-induction and expected-VIOLATION tasks incremental BMC, both with a scan-cycle watchdog.The harness attempted all 50 benchmarks and recorded outcomes for every variant.Source: §6 · p. 7
6.1 Results
- 45 accepted variants ran, including all 25 graphical benchmarks; 43 matched recorded verdicts, while two safe edge-detector outcomes remained UNKNOWN.The UNKNOWN outcomes reflect k-induction proof strength and are not counted as SAFE.Source: §6.1 · p. 7
6.2 A Format-and-Semantics Finding
- 38 textual-Ladder and ST variants did not run: the frontend rejects their formats, and timer, counter, and latch semantics can differ from the independent reference semantics.Porting these cases requires re-establishing ground truth under each tool’s timing model, not merely re-serializing programs.Source: §6.2 · p. 7
6.3 Cross-Tool Confirmation
- Across 24 variants, nuXmv agrees with ESBMC-PLC and recorded ground truth; it also proves two edge-detector benchmarks that ESBMC-PLC leaves UNKNOWN.The comparison covers finite-state cases using unrelated decision procedures, with nuXmv models translated from PLCopen XML to SMV.Source: §6.3 · p. 7, Table 4 · p. 8
6.4 Scope of These Numbers
- Cross-tool comparison covers 15 finite-state graphical benchmarks; non-terminating tank controllers and textual-LD and ST benchmarks remain single-tool.A complete multi-tool matrix across all three languages and XML normalization for tool ingestion remain outstanding.Source: §6.4 · p. 8
6.5 Validation Coverage
- 31 of 50 benchmarks are validated, while 19 remain candidates, concentrated in semantics-dependent timer/counter/latch features and ST programs not yet encoded for a second checker.Empirical claims concern the validated set; per-task status enables reweighting by domain or provenance.Source: §6.5 · p. 8
7 Threats to Validity
The threats analysis identifies limits in property and fault-model coverage, residual uncertainty in labels, constrained generalizability, and cross-tool format fragmentation. It describes mitigations including published justifications, per-domain reporting, and end-to-end rechecks.
7.1 Construct Validity: Do the Tasks Measure Verification Capability?
- Most benchmarks carry one property, so the suite measures selected safety obligations rather than full functional correctness.The 34 VIOLATION variants comprise 14 scan non-terminations, 14 safety-invariant violations, and 6 interlock violations; the public corpora supply only non-termination defects, while other classes use authored or curated mutants.Source: §7.1 · p. 8
7.2 Internal Validity: Are the Expected Verdicts Correct?
- 31 verdicts are validated and 19 remain candidates; SAFE consensus labels require a tool-independent basis, and UNKNOWN is not treated as SAFE.The authors publish justifications and witnesses for independent checking; only 18 of 83 variants rely on consensus, in which ESBMC-PLC also participates as the baseline.Source: §7.2 · p. 9
7.3 External Validity: Do Results Generalize?
- 31 of 50 benchmarks are authored, water treatment accounts for 16 of 50, and heavy scalability stress rests on two program families.The authors include 19 third-party or prior programs, ensure each domain has at least two genuine anchors, and report results per domain; five syntax-coverage twins are counted once per language slice.Source: §7.3 · p. 9
7.4 Reproducibility
- A single command rechecks verdicts, but differing input formats prevent any one baseline checker from running on all 50 programs.The authors report per-tool coverage rather than dropping unsupported rows, and archive the corpus and harness at the exact baseline tool commit.Source: §7.4 · p. 9
8 Conclusion
The paper presents a property-bearing benchmark suite for IEC 61131-3 verification and a ground-truth discipline motivated by a misclassification of non-terminating logic bombs. It also sets out plans to confirm candidate verdicts, expand cross-tool comparisons, and broaden the corpus.
8 Conclusion
- The suite covers 50 benchmarks and 83 variants across textual and graphical LD and ST in ten industrial fields, with properties, expected verdicts, and violation witnesses.It is presented as the first formal-verification benchmark suite to cover graphical LD and is packaged in an SV-COMP-compatible layout with a validator and recheck harness.Source: §8 · p. 9
- An obvious valve-interlock property would label public logic-bomb variants SAFE because their injected non-terminating loops leave valve logic intact.The paper records each task's ground-truth provenance as construction, fault injection, or audited cross-tool consensus.Source: §8 · p. 9
- The authors plan to tool-confirm 19 candidate verdicts under each tool's semantics, allowing timer-dependent verdicts to differ and recording both.They also plan a full PLCverif, nuXmv, and ESBMC-PLC matrix after normalizing the corpus to a PLCopen XML form accepted by every frontend.Source: §8 · pp. 9–10
- Further planned work includes broadening the fault model, adding programs from proprietary vendor toolchains, and enlarging the corpus for a standing competition category.The stated aim is a shared, extensible foundation for measuring and comparing PLC formal-verification progress.Source: §8 · p. 10
Declarations
The declarations report the work's funding and identify the openly available benchmark artifacts.
Declarations
- The work was partially funded by EPSRC grants EP/T026995/1, EP/V000497/1, and EP/X037290/1, and by the Soteria project under the DSbD Programme.Source: Declarations · p. 10
- The complete benchmark suite, including programs, properties, witnesses, schema, validator, and recheck harness, is openly available.Source: Declarations · p. 10