Write once, model check everywhere: an UPPAAL front-end for LTSmin

Update the opaal role for the modern toolchain: use UTAP to parse UPPAAL XML models and translate them to LTSmin’s PINS specification, so that discrete (clockless) UPPAAL models can be checked in LTSmin. Validate on a set of selected examples.

Picture of alex-potanin.md Alex Potanin

1 Sep 2026

Motivation

Mainstream model checkers were mostly built 10–20 years ago. They’re powerful, but their architecture predates modern software-engineering practice and could serve it far better. They usually couple three things that are conceptually separate: a modelling language (UPPAAL XML/XTA, Promela, SMV, TLA+), a state-space semantics, and a set of checking algorithms. In practice this coupling means a model is locked to its tool: verifying the same design in a second checker requires a hand-translation into that tool’s language, which is expensive, drifts from the original, and — as this project’s own history shows — never reproduces the same raw state counts, making independent confirmation of a verdict hard to trust. Each model checker has its own strengths, but the coupling forbids composition: switching checkers means manual translation every time, there is no way to check two models for equivalence, and keeping them consistent as either one evolves is a constant headache. Our echo-server case study has lived this problem directly — it has been modelled by hand in UPPAAL, Spin, NuSMV, and TLA+, precisely because no infrastructure existed to check one model with several engines.

LTSmin is the architectural answer to this coupling: its PINS interface (Partitioned Interface to the Next-State function) decouples language front-ends from algorithm backends, so any language that can expose “state vector + next-state + dependency matrices” gets LTSmin’s entire algorithm suite — explicit-state, multi-core, symbolic, LTL — for free, plus ltsmin-compare bisimulation between state spaces from different front-ends. Promela already has a working front-end (SpinS). The UPPAAL front-end (opaal) is dead: fetchable only via Bazaar + Python 2 from Launchpad, with no usable mirror.

What makes rebuilding the UPPAAL bridge tractable now is that UPPAAL has open-sourced its own components: UTAP, the official parser/typechecker (LGPL, maintained), and UDBM, the official DBM library. The bridge no longer needs to reimplement UPPAAL’s language or its zone arithmetic — it can be built on the same components UPPAAL itself uses, and only the translation to PINS remains to be written. That translation is this project.

Goal

Update the opaal role for the modern toolchain: use UTAP to parse UPPAAL XML models and translate them to LTSmin’s PINS specification, so that discrete (clockless) UPPAAL models can be checked in LTSmin. Validate on a set of selected examples, conformance-testing the model-checking results against UPPAAL’s own verifyta and against LTSmin.

Bonus (attempt only if ahead of schedule after the core goal above):

  1. Integrate timed semantics via UDBM. Zones embedded in the PINS state, LU-extrapolation for termination, LTSmin subsumption; validated on UPPAAL’s classic timed demos (train-gate, Fischer).
  2. Cross-tool bisimulation. Compare the UPPAAL model and the Spin model of the same example using LTSmin’s bisimulation checking, to identify any discrepancies between them.

Deliverable

  • A reproducible build of LTSmin + UTAP (optionally UDBM as well) with the module in-tree.
  • Cross-tool comparison: run conformance tests on selected UPPAAL examples, comparing verification results and performance between the two backends — UPPAAL’s verifyta and LTSmin.
  • The final report.

Requirement

  • Proficiency in a systems programming language (Rust, C++, or C).
  • Basic familiarity with model checkers and automata/transition systems.

What you will learn

Real engineering practice: programming skill, software-architecture judgement, and hands-on experience integrating with and contributing back to an open-source project, including working through GitHub’s collaboration workflow (issues, PRs, code review).

Take-home questions

  • Technical decision: PINS in LTSmin is implemented in C, UTAP is implemented in C++, and Fiducia — a prospective future consumer of this work — is written in Rust. Which implementation language best fits this landscape, and what architecture should tie them together? Think through the trade-offs across reusability, long-term maintenance, and soundness.

References

arrow-left bars magnifying-glass xmark