Source linked

SMT Solver Shuts Vacuous Verification of PLC Ladder Diagrams

arxiv.org@systems_wire2 hours ago·Systems Engineering·2 comments

Previous ESBMC-PLC parsed graphical ladder diagrams into empty IR, silently passing all checks. Graph-ESBMC-PLC's DFS resolver now extracts real rung logic and verifies correctness via SMT in under 70ms.

graph esbmc plcesbmcplcopenformal verificationprogrammable logic controllerssmt model checking

Three ladder diagram programs from CONTROLLINO and OpenPLC Editor previously sailed through ESBMC-PLC with an empty intermediate representation and a vacuous 'SAFE' verdict. That bug is now dead.

The Empty IR Bug

ESBMC-PLC handled textual PLCopen XML just fine - 11 benchmarks all passed. But when you fed it a graphical LD export from CONTROLLINO, Beremiz, or OpenPLC Editor, the parser produced an empty GOTO IR. Model checking then trivially succeeded on nothing, making every ladder program look safe by default. Vacuous verification at its worst.

The root cause was a textual-only encoding assumption. PLCopen XML defines two formats: a text-based element encoding and a graphical encoding that stores rung logic as a directed graph of localId/refLocalId connections. ESBMC-PLC only understood the former.

How Graph-ESBMC-PLC Traces the Rungs

Graph-ESBMC-PLC closes the gap with a DFS-based graphical LD resolver. It walks the connection graph from leftPowerRail to each coil, extracting rung paths as Boolean contact conjunctions. A three-tier I/O inference scheme sorts out signal directions. Coils are ordered by rightPowerRail connectionPointIn sequence, ensuring SET coils are processed before RESET coils - matching IEC 61131-3 scan-cycle semantics exactly.

The resolver's output feeds the unchanged ESBMC backend. No backend modifications needed.

What the Benchmarks Show

Three graphical LD programs from CONTROLLINO and OpenPLC Editor now produce a full GOTO IR with nondeterministic inputs and rung logic. All three verify SAFE at an unwind depth k=2 in under 70ms. The 11 textual LD benchmarks remain fully preserved with zero regression.

Two Beremiz examples are flagged as known limitations: one has no LD content, the other uses unsupported timer semantics. The authors note these as discovered limitations rather than bugs.

The artifact is available on Zenodo (DantasCordeiro2026graphical, doi:10.5281/zenodo.20699856).

Graph-ESBMC-PLC now makes formal verification of graphical PLC programs practical for production use - assuming the toolchain handles Beremiz timer semantics next.

Source: Graph-ESBMC-PLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking
Domain: arxiv.org

Read original source ->

External source stays available while the OJO article and comment thread stay local.

More in Systems Engineering

view topic
LLM Anchoring Bias Wastes 25% Energy in 6G Network Slicing

A randomized anchoring strategy using a Truncated Weibull distribution eliminates rigid negotiation patterns, cutting energy waste from LLM-driven 6G slicing while keeping inference under one second on a 1B-parameter...

Mozilla's Perfherder Misses 6.8% of Regressions, CPD Ensembles Fix That

An evaluation of 25 change-point detection methods on Mozilla production data shows ensemble voting cuts false positives and recovers missed regressions, boosting F1-score by 11%.

CHERI-D Inlines Object IDs for Fast Use-After-Free Prevention

CHERI-D stores object IDs inline with allocation data using unused fragmentation, cutting revocation overhead versus Cornucopia Reloaded while enabling strict use-after-free protection.

HPC FFT Library Beats FFTW by 4x Using Quantum Circuit Simulation

QFT→FFT maps input arrays to quantum state amplitudes and runs on Google's qsim, matching FFTW on AVX and beating it 4x on an A100.

Comments load interactively on the live page.