💬 NLP

ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking

This paper introduces ESBMC-GraphPLC, a formal verification tool that resolves the gap in handling graphical PLCopen XML Ladder Diagrams by implementing a DFS-based resolver to convert graph-based rung logic into a valid GOTO intermediate representation for SMT-based model checking, thereby enabling correct verification of programs from editors like CONTROLLINO and OpenPLC Editor without affecting existing textual format support.

Original authors: Pierre Dantas, Lucas Cordeiro, Waldir Junior

Published 2026-06-19

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Pierre Dantas, Lucas Cordeiro, Waldir Junior

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine a Programmable Logic Controller (PLC) as the brain of a factory machine, like a water pump or a traffic light. To tell this brain what to do, engineers draw Ladder Diagrams. These look like electrical ladders with rungs, where each rung is a rule: "If the water tank is full, turn off the pump."

For a long time, there were two ways to save these ladder drawings on a computer:

The Text List: A simple, step-by-step list of instructions (like a recipe).
The Graphical Map: A visual map where pieces are connected by invisible wires, identified by ID numbers (like a subway map where stations are connected by lines).

The Problem: The "Ghost" Program

The researchers had a powerful tool called ESBMC-PLC that could check these programs for safety errors. It worked perfectly on the Text List format.

However, when they fed it the Graphical Map format (which is what modern software like CONTROLLINO and OpenPLC actually uses), the tool got confused. It looked at the map, saw the ID numbers and wires, but couldn't figure out how they connected.

Because it couldn't read the map, it assumed nothing was happening. It thought every switch was off and every pump was stopped.

The Result: The tool said, "Everything is safe!"
The Catch: It was lying. It wasn't safe because the logic was missing; it was "safe" because the tool was looking at an empty room. This is called vacuous verification—it's like saying a locked door is secure because you forgot to check if there's a window open.

The Solution: ESBMC-GraphPLC

The authors built a new module called ESBMC-GraphPLC to fix this. Think of it as hiring a detective to walk through the graphical map and translate it back into a language the safety checker understands.

Here is how their "detective" works, using simple analogies:

1. The Detective with a Flashlight (DFS Algorithm)
The tool uses a method called Depth-First Search (DFS). Imagine a detective walking through a maze of wires. They start at the left side of the ladder (the power source) and follow every possible path to the right side.

They trace every wire connection.
They write down every switch (contact) they pass.
They stop when they reach the device (the coil/pump).
By doing this, they reconstruct the exact logic of the ladder rung, turning the visual map back into a clear "If-Then" rule.

2. The Traffic Cop (Ordering Matters)
In these diagrams, sometimes you have a "Set" switch (turn on) and a "Reset" switch (turn off) for the same device. The order matters!

If the "Reset" happens after the "Set" in the same split second, the device stays off.
If the "Set" happens after the "Reset," the device stays on.
The new tool looks at a specific list in the file (the rightPowerRail sequence) to see which switch comes first, acting like a traffic cop ensuring the "Set" car goes before the "Reset" car. This ensures the logic matches how real machines actually behave.

3. The Guessing Game (I/O Inference)
Sometimes the map doesn't say which wires are "Inputs" (sensors) and which are "Outputs" (motors). The tool uses a three-step guessing game:

Step 1: Look for official address labels (like %IX for inputs). If found, it's exact.
Step 2: If no labels, look at the behavior. If a wire is only used as a switch, it's probably an input. If it's only used to turn something on, it's probably an output.
Step 3: If still unsure, treat it as a "mystery variable" that could be anything. This is a safe bet because it checks all possibilities, ensuring nothing is missed.

The Results

The team tested this new detective on three real-world programs (water pumps, stair lights, and dimmer lights).

Before: The tool saw an empty room and said "Safe" (incorrectly).
After: The tool saw the full logic, checked every possible combination of sensor inputs, and confirmed the programs were actually safe.
Speed: It did this in less than 70 milliseconds (faster than a human blink).
Safety: It didn't break the old tool. The 11 programs that were already working with text lists still worked perfectly.

What It Can't Do Yet (The Limitations)

The paper is honest about what the detective still struggles with:

Complex Timers: If a rung involves a timer (e.g., "Wait 5 seconds, then turn on"), the tool currently ignores the "wait" part and treats it as a random guess. It's safe, but it doesn't understand the timing.
Nested Maps: Some complex diagrams hide smaller maps inside other sections (like actions inside a step). The detective sometimes misses these hidden rooms.

Summary

In short, the authors built a translator that allows safety-checking software to finally "read" the visual ladder diagrams used by modern industrial software. They turned a tool that was blindly saying "Everything is fine" into a tool that actually understands the logic and can prove the machine won't break or hurt anyone.

Technical Summary: ESBMC-GraphPLC

Problem Statement
The paper addresses a critical gap in the formal verification of Programmable Logic Controller (PLC) programs using the ESBMC-PLC tool. While ESBMC-PLC successfully supported the textual format of PLCopen XML (tc6_0201), it failed to correctly process the graphical format, which is the native export format for major development environments like CONTROLLINO, Beremiz, and OpenPLC Editor.

In the graphical format, Ladder Diagram (LD) logic is encoded as a directed graph of localId and refLocalId connections rather than explicit <rung> elements. The existing parser detected these files but found no rungs, resulting in an empty GOTO Intermediate Representation (IR). Consequently, all variables remained zero-initialized, causing verification to succeed vacuously: properties trivially held because no logic was generated. This provided no actual guarantee regarding the safety of the PLC logic.

Methodology
The authors introduce ESBMC-GraphPLC, a module that bridges this gap by implementing a Depth-First Search (DFS) based resolver to reconstruct rung logic from the graphical connection graph. The methodology involves three core components:

Graphical LD Resolver & Rung Extraction:
- The system parses the localId/refLocalId graph to identify paths from the leftPowerRail to each coil.
- It traverses the graph to extract sequences of contacts, converting them into Boolean conjunctions.
- Critical Ordering Insight: To adhere to IEC 61131-3 scan-cycle semantics, the algorithm orders coil processing based on the sequence of refLocalId entries in the rightPowerRail's connectionPointIn list. This ensures that SET coils are processed before RESET coils within the same scan cycle, preserving correct latch behavior.
Three-Tier I/O Inference:
To correctly model inputs (nondeterministic re-sampling) and outputs (persistent state), the tool employs a tiered classification scheme:
- Tier 1: Uses explicit IEC 61131-3 hardware addresses (%IX for inputs, %QX for outputs).
- Tier 2: Applies a heuristic analysis for address-free programs, classifying variables appearing only as contacts as inputs and those appearing only as coils as outputs.
- Tier 3: Treats unclassified variables as internal persistent state.
Implementation Strategy:
The solution is implemented entirely within the frontend parser (plcopen_xml_parser.cpp, +274 lines). It requires zero changes to the ESBMC backend, including the GOTO IR encoder, k-induction engine, Z3 SMT solver, or property encoder. The resolver outputs a standard RungNode list, identical to the structure produced by the textual parser.

Key Contributions

Formal Model: A formal definition of the graphical LD connection graph and a soundness theorem proving that the DFS-extracted paths are equivalent to IEC 61131-3 scan-cycle semantics.
Algorithmic Solution: The first open-source implementation of a DFS-based rung extractor for graphical PLCopen XML that correctly handles SET/RESET ordering.
Backward Compatibility: The extension preserves all existing functionality for textual LD benchmarks with zero regressions.
Artifact: A complete, reproducible artifact including the tool, benchmarks, and a Python prototype for validation.

Experimental Results
The tool was evaluated on 3 graphical LD programs exported from CONTROLLINO and OpenPLC Editor:

Water Control (water_control): 5 rungs (2 SET, 3 RESET).
Staircase Light (stairs_light): 6 rungs (2 SET, 2 RESET, 2 plain).
Dimmer Light (dimmer_light_control): 4 rungs (plain).

Outcomes:

IR Completeness: All 3 programs transitioned from producing an "Empty IR" (vacuous) to a "Full IR" containing nondeterministic inputs and full rung logic.
Verification: All 3 programs verified SAFE at $k=2$ in under 70 ms (median times: 50ms, 40ms, 60ms).
Regression: The 11 genuine textual LD benchmarks from ESBMC-PLC produced identical results, confirming zero regressions.

Limitations and Scope
The paper explicitly notes that the current resolver does not preserve the semantics of function blocks (timers, counters, comparators) within rung paths. If a rung relies on a function block, the tool treats the block's output as a nondeterministic term (sound over-approximation) or, in specific cases like the beremiz_traffic_light example, the logic collapses to a constant. Two Beremiz examples were excluded from the main results to avoid reporting misleading "SAFE" verdicts for programs where timing semantics were lost.

Significance
The paper claims that ESBMC-GraphPLC enables the sound, non-vacuous formal verification of graphical PLCopen XML programs, which are the standard output of modern PLC development environments. By closing the gap between graphical exports and SMT-based model checking, the tool allows automation engineers to verify safety properties (e.g., pump control, traffic lights) without manual conversion to textual formats. The authors emphasize that while the current implementation handles contact/coil networks with SET/RESET latches effectively, future work is required to integrate function-block semantics to support more complex sequential control logic.