Formal Error Detection on State Machines: What Works and What Doesn't

Model-based development shifts errors earlier in the process — but that alone is not enough. Logical bugs can still hide inside the model itself, ones no test will ever uncover: states that are never reached; conditions that can never be true; value ranges that silently overflow. In 1996, a single unchecked range conversion was enough to destroy Ariane 5 thirty-seven seconds after launch. In systems that no one can patch after deployment, that is the most expensive way to find a bug.

The value of formal error detection is therefore beyond question. What is interesting is whether it can be applied practically to state machines. We tried that in two master’s theses at TU Dortmund, using itemis CREATE as the test bed. Here we take a closer look at the overall results: what these methods deliver, where they run into limits, and what is useful in the end.

Reachability as a Satisfiability Problem

The core idea is a Symbolic Execution Tree (SET). Instead of concrete inputs, the analysis works with symbols. For each path through the tree, it maintains a path condition: the conjunction of all guards and assignments along that path. Each node captures the symbolic state: variable values plus the current path condition. Successor nodes are generated by applying transition rules or expression rules that fold guards and assignments into the path condition.

Reachability reduces to satisfiability. A state is reachable if at least one path in the tree has a satisfiable path condition. An SMT solver (in our case Z3) handles this check. If Z3 returns UNSAT for every path to a transition, that transition is unreachable.

This maps the interesting bug classes to small, precise solver queries:

• Contradictory guard: the guard g is unsatisfiable. The solver checks sat(g). UNSAT means the transition never fires under any variable assignment.
• Tautological guard: the guard is always true. Checked via unsat(¬g). If the negation is unsatisfiable, the guard is redundant.
• Shadowing: two transitions t1 (higher priority) and t2 from the same state on the same event. t2 is shadowed if g(t2) ∧ ¬g(t1) is unsatisfiable: every assignment that would trigger t2 also triggers t1.

• Division by zero: for each divisor d on a path, the solver checks sat(pc ∧ d == 0). If satisfiable, there’s a reachable path where d can be zero.
• Dead state: a reached state whose outgoing guards are all unsatisfiable under the current path condition.

• Infinite loop: a cycle whose exit condition is never satisfiable, leaving the states behind it unreachable.

One property is non-negotiable: a reachable state must never be reported as unreachable. The analysis is conservative: it only reports “unreachable” when it can prove it. There are no false positives on unreachability. That is the prerequisite for trusting the tool.

The symbolic execution tree grows exponentially — without pruning, the analysis does not terminate. Limiting depth or paths risks blind spots: bugs in deeply nested paths remain invisible, not because they do not exist, but because the tree no longer reaches them. The depth limit is the central control for this trade-off.

Which Method Works

Three requirements narrowed the field: the check should run directly on the model in the editor — no separate translation step. It should be able to handle arithmetic data, because our bug classes (unsatisfiable guards, division by zero) fall in the domain of an SMT solver, not a control-flow checker. And it should work with the statechart model of itemis CREATE without simplifying it first.

The established approach for this problem is model checking. The main tools are SPIN (modeling in Promela, properties in Linear Temporal Logic) and UPPAAL (timed automata for real-time systems). Both are proven in industry: SPIN in the flight software of NASA’s Deep Space 1 probe, UPPAAL wherever hard timing constraints apply. For temporal properties of concurrent or time-sensitive systems, they are the first choice.

Specifically designed for statecharts is the Gamma Statechart Composition Framework from TU Budapest (FTSRG). Gamma uses itemis CREATE as its frontend: components are modeled directly there, Gamma compiles them into an intermediate language and translates them to backends like UPPAAL, Theta, Promela, or SMV. The same model also generates Java code. Composite and orthogonal states (which our prototype omitted) are part of Gamma’s core feature set.

For our specific goal, this approach was not a good fit. First, it requires a translation step: the statechart is converted to another format instead of being checked directly in the editor. Second, the backends deliberately abstract away data; SPIN doesn’t even have a notion of time. But data-oriented bug classes (unsatisfiable guards with integer arithmetic, division by zero, dead states) fall squarely in the SMT solver domain. That is why we looked at the SMT and symbolic execution family.

Three approaches were candidates:

Pure SMT solving. Pass the guard directly to Z3. Fast and exact for local properties like contradictions, tautologies, and shadowing. For a full reachability analysis over the entire model, there is no framework to generate paths and runtime states.

Deductive verification with Dafny. In theory, the strongest option. In practice, not viable here: Dafny requires every program’s termination to be provable. A reactive state machine that waits indefinitely for events does not fit that constraint. The approach also produced false positives.

Program verification with KeY. Operating on generated Java code, it handles non-terminating automata better, finds dead states and divisions by zero, and can be embedded directly as a Java program. The weakness: arbitrary loops can hang the verifier.

KeY came closest, but the path via generated Java code again means a translation step — and arbitrary loops can hang the verifier. The combination of symbolic execution and SMT solving fixes exactly that: symbolic execution builds the path tree directly on the model without requiring termination. The SMT solver checks the path conditions — without the data blind spots of SPIN or the termination requirement of Dafny. This is exactly the same architecture used by established code-level tools like KLEE and EXE.

The Wall: State Explosion

This depth limit is not an arbitrary constraint — it is the direct response to a structural problem. Symbolic execution traces all paths simultaneously, and that does not scale well. Every branch can double the path count in the worst case; every cycle can in principle generate infinitely many. Model checking calls the same phenomenon state explosion. It is the obstacle the field has been working on for decades, with ML-guided path selection, state merging, coupling to bounded model checking, and concolic execution — the mix of symbolic and concrete execution — as responses. For statecharts with arithmetic guards, none of these apply directly: concolic execution requires executable code; bounded model checking abstracts away data.

We bound the tree through cycle elimination. The analysis finds cycles via the strongly connected components of the transition graph — sets of states that can mutually reach each other. Naively, resolving a cycle would discard all variable knowledge. The key insight: only forget knowledge about variables that actually change within the cycle. Everything else is preserved, so the solver can keep working with the stable values.

You can choose between conservative elimination, which allows a configurable number of cycle passes before cutting (more precise but slower), and preemptive elimination, which cuts at the first visit (faster but less precise). Cycles from local reactions are handled too, not just transitions. The tradeoff is always the same: some precision for guaranteed termination.

What Makes It Fast Enough

The solver call dominates runtime. Four optimizations made the biggest difference:

• Independence optimization. A path condition often decomposes into subsets of constraints that share no variables. For a specific query, the solver only needs to check the relevant subset, not the entire condition. This is the same idea used in KLEE and EXE under the name constraint independence.
• Satisfiability result caching. Identical or embedded sub-conditions reappear throughout the tree. A cache eliminates redundant solver calls.
• Context-aware solving. Known constraints are passed as context instead of solving each query from scratch.
• Path cost function. The engine prioritizes paths that are most likely to reveal new reachability results.

Models are serialized to SMT-LIB2; Z3 and jConstraints served as solver backends. In 2020, no comparable engine existed for statecharts as models — we therefore built one from scratch, modularly, with pluggable strategies for exploration and satisfiability checking.

Results:

• The fastest strategy stayed under 0.2 seconds for up to around 6,800 nodes and edges.
• Tests covered all components and reached 85% code coverage.
• Additional analyses run on the same execution tree without recomputing it, including uninitialized variable detection and, most valuably in perspective, test case generation that covers all execution paths.

And the limits, honestly stated:

• Composite and orthogonal states, history nodes, and multiple regions are not supported.
• External function calls are not analyzed.
• Evaluation used a synthetic automaton, not a production model.
• The practical upper bound of around 6,800 nodes comes from the strongly connected component computation.

Context

Formal verification has long been standard practice in safety-critical domains. DO-178C (aviation), EN 50128 (rail), ISO 26262 (automotive), and IEC 61508 all require evidence that software behaves as defined and produces no unexpected outputs.

What these standards have in common: they only accept statements that are provable — not ones that are merely likely to be true. The decisive criterion is therefore completeness. Formal verification in the sense these standards intend requires a complete analysis: either a property is proven, or a counterexample is produced. The approach described here (symbolic execution with cycle elimination) does not satisfy this. It is conservative: what it marks as unreachable is unreachable. But it is not complete: what it does not find may still exist. That makes it a useful companion during development, not a substitute for standards-compliant formal verification.

Conclusion

The feasibility is established, with clear boundaries. Local bugs like unsatisfiable guards, tautologies, and shadowing are found quickly and exactly by an SMT solver. A full reachability analysis over the entire model is practical with symbolic execution and an SMT solver, as long as path explosion is controlled through cycle elimination, trading some precision for guaranteed termination. For day-to-day development work, this approach is sufficient.

The analysis is conservative: what it reports as unreachable is unreachable. That enables a different mode of use from classical verification: not a one-time gate check before release, but a permanent background check in the editor. An unsatisfiable guard becomes visible while it is being written, not after the model has already flowed into other artefacts. The earlier a bug is found, the cheaper it is to fix — that is true for code, and it is true for models.

The state machine was just our test bed. Undecidability, path explosion, and the tradeoff between completeness and practicality apply to formal verification in general, regardless of the model type.

Sources

We investigated feasibility in two master’s theses at the Software Engineering chair (LS-14) at TU Dortmund, supervised by Prof. Dr. Jakob Rehof and Dr.-Ing. Martin Hentschel, in cooperation with itemis (Dominic Starzinski, 2019; Jonas Wielage, 2020).

Model-Driven Software Development at itemis: Analyze, validate, and generate code from state machines: Model-Driven Software Development →