A Benchmark Suite and Ground-Truth Methodology for Formal Verification of IEC 61131-3 Ladder Diagram Programs
Pierre Dantas, Lucas Cordeiro, Waldir Junior
cs.CL · cs.AR · cs.SE
Quick verdict
First graphical-LD PLC verification benchmark with triangulated ground truth; credible and honest, but cross-tool validation is narrow and self-referential.
Summary
The paper presents a 50-program (83-variant) benchmark suite for formal verification of IEC 61131-3 PLC programs, covering textual Ladder Diagram, graphical LD (PLCopen XML), and Structured Text across ten industrial domains; each task pairs a program with a formal property (invariant/termination/mutual-exclusion/reachability), a machine-checkable expected verdict, and an SV-COMP-style violation witness. Its core contribution is a ground-truth methodology assigning every verdict to construction, fault injection, or audited cross-tool consensus, motivated by an episode where the obvious valve-interlock property mislabelled all logic-bomb attacks in two public corpora as SAFE because the injected defect is a non-terminating loop, detectable only via a scan-cycle termination property. Reference verdicts came from ESBMC-PLC v8.4: all 25 graphical benchmarks ran, 43/45 accepted variants matched with zero disagreements, and nuXmv 2.2.0 independently agreed on all 24 interlock variants and resolved two ESBMC UNKNOWNs. Main limitations: 38 of 83 variants (all textual-LD/ST) could not run on the reference tool due to format and timer-semantics fragmentation; 19 benchmarks remain 'candidate' (tool-unconfirmed); cross-tool coverage spans only 15 finite-state benchmarks; ESBMC-PLC is the authors' own tool and the audits are authorial. Full multi-tool normalization is deferred as future work.
Review complete
Assessment at a glance
5
risk flags identified
● high 0
● medium 3
● low 2
5 strengths · 5 weaknesses · 5 author questions
Levels reflect verification complexity — not a quality score. Evolve never rates your paper.
Key claims under review
- The suite is the first formal-verification benchmark for IEC 61131-3 programs to cover graphical Ladder Diagram, pairing 50 programs (83 variants) with formal properties, machine-checkable expected verdicts, and SV-COMP-style violation witnesses.
- Every expected verdict is established by one of three recorded methods — construction, fault injection, or audited cross-tool consensus — because the obvious safety property mislabels all logic-bomb attacks in two public corpora as SAFE, the injected defect being a non-terminating loop invisible to valve interlocks.
- ESBMC-PLC v8.4 runs all 25 graphical benchmarks and matches 43/45 accepted variant verdicts with zero disagreements, while nuXmv independently agrees on all 24 interlock variants and resolves two benchmarks ESBMC leaves UNKNOWN, evidencing tool-neutral ground truth and suite-level discrimination.
- The tool ecosystem is fragmented in input format and even in the semantics of standard timers, and the suite is explicitly designed to measure this fragmentation.
Strengths
Real, previously unserved gap: first property-bearing suite for graphical LD
§2/§4: prior resources are program corpora without verdicts (PLC-LD, SWaT/PLC_Defuser, PPU clone set) or ST-only with properties (Ukegbu & Mehrpouyan, 40 ST programs). The 25 graphical PLCopen XML benchmarks, each with a formal property, expected verdict, and witness, are the first verification tasks targeting the encoding in which real PLC programs are exchanged.
Ground-truth methodology grounded in a concrete, checkable failure mode
§5 documents that the obvious valve-interlock property would label every malicious variant of both ingested corpora SAFE, because the injected defect is uniformly a non-terminating loop (e.g. i := i*i) leaving functional logic untouched. The resulting termination property class (14 variants, discharged by a scan-cycle watchdog) is a property kind absent from all prior PLC benchmarks, and the lesson generalizes beyond PLCs.
The suite discriminates tools, not merely confirms them
Unusual transparency about the suite's weak spots
SV-COMP-aligned infrastructure lowers adoption cost
Weaknesses
Cross-tool validation is narrow relative to the headline framing
Self-referential ground truth and audit
As released, no single tool can run the suite end-to-end
Modest scale and narrow real-world fault model
Cross-tool agreement may partly reflect a shared translation
Full Review Report
$1.99 · one-timeUnlock the complete preliminary analysis Evolve produced for this paper.
- All 5 strengths & 5 weaknesses, analyzed in detail
- 5 risk flags with severity, section & reviewer questions
- Methods & statistical evidence assessment
- 5 questions a peer reviewer would ask
- Full six-dimension evaluation report & recommendations
One-time purchase · this paper only
One-time purchase, this paper only. AI-generated preliminary analysis — not peer review.
Frequently asked questions
What is this paper about?
It introduces a public benchmark suite of 50 PLC programs (83 variants) for testing formal verification tools on IEC 61131-3 Ladder Diagram and Structured Text code. Each program comes with a formal property, a machine-checkable expected verdict (safe or violation), and a counterexample witness, packaged in the same layout as the SV-COMP software verification competition so new tools can plug in via adapters.
Why is establishing ground truth hard for PLC verification benchmarks?
Because the correct verdict is not obvious even for small controllers. In two public 'logic bomb' corpora the paper ingests, every malicious variant hides its attack as a non-terminating loop while leaving the safety logic intact, so the obvious valve-interlock property would classify all attacks as safe. The authors therefore label each verdict by construction, fault injection, or audited cross-tool consensus, and add scan-cycle termination as an explicit property class.
Which verification tools were used and what were the results?
Reference verdicts were produced with ESBMC-PLC v8.4: all 25 graphical (PLCopen XML) benchmarks ran and 43 of 45 accepted variants matched the recorded verdict, with two reported as unknown. The independent model checker nuXmv 2.2.0 agreed on all 24 interlock variants and proved two edge-detector benchmarks ESBMC left unknown. The 38 textual-Ladder and Structured Text variants could not run due to input-format and timer-semantics differences between tools.
Is the benchmark suite publicly available?
Yes. The paper states the corpus, property files, witnesses, JSON schema, validator, and one-command recheck harness are openly released at github.com/pierredantas/esbmc-plc-benchmark-suite and archived under a citable DOI at the exact tool commit used for the baseline (no DOI identifier is printed in the paper text itself).
About this review
This is an AI-generated preliminary review by Evolve.Pub, produced from the openly available text of the paper. It is not peer review and does not represent the authors' views. The canonical record of the paper is at the publisher link above.
- Review is based on extracted text only: Figure 1 is available only through its caption, and Tables 1-4 were parsed inline, so layout and any per-benchmark appendix data could not be checked.
- The released artifact (GitHub repository / DOI) was not inspected; the 'high' reproducibility rating reflects the paper's described infrastructure (schema, validator, run_all.sh, adapters), not verification of the archive itself.
- No DOI identifier appears in the provided text despite the 'archived under a citable DOI' claim, so availability statements are taken at face value.
- Tool-version claims (ESBMC v8.4, nuXmv 2.2.0) and all reported counts could not be independently re-run within this review.
Go deeper on this paper
Wrote a paper? Stress-test it before reviewers do.
Upload your manuscript for the same structured scrutiny — reasoning, statistics, evidence, figures, and reproducibility.