Motivation
Model checking is a way of proving things about a concurrent system — that it never deadlocks, that a safety property always holds — by exhaustively exploring every state it can reach, rather than testing a sample of behaviours and hoping. Spin is one of the most widely used model checkers: systems are described in a language called Promela (processes, channels, shared variables), and Spin explores the full space of ways those processes can interleave, checking for violations along the way.
LTSmin is a different kind of tool: instead of understanding any one modelling language itself, it provides a common interface — called PINS — through which many different languages can plug in, and in return get access to LTSmin’s own high-performance checking algorithms (multi-core search, symbolic/BDD-based search, LTL/CTL/temporal-logic checking) that a single-language tool like Spin doesn’t have on its own. Each language needs a “front-end”: a translator from that language into PINS. For Promela, that front-end already exists — a tool called SpinS — so nobody has to build one from scratch here. That sounds like the hard part is already done. It isn’t, and that’s what this project is about.
SpinS hasn’t been touched since 2018, and Promela’s own semantics have moved since then. A translator that quietly drifts from what its source language actually means is more dangerous than one that doesn’t exist at all: a missing tool is an obvious gap, but a stale one keeps producing confident-looking verdicts for the wrong model, with nothing in the output to say anything is wrong. This already happened once on this project’s own models: a scheduling feature called priority, which is supposed to restrict which interleavings are even considered, was silently ignored by SpinS — so a model that used it looked like it deadlocked, a false alarm that took real effort to trace back to its actual cause. Until gaps like this are closed, “checked via SpinS/LTSmin” and “checked via Spin itself” are not provably the same check on the same model — which is precisely the property anyone relying on this bridge needs to be able to trust.
Goal
Repair SpinS’s known gaps between what it implements and what Promela actually means, and build a conformance test suite: a fixed corpus of Promela models run through both native Spin and SpinS/LTSmin, comparing verification verdicts (deadlock, reachability) and performance. Three known gaps, fixed in order of increasing difficulty:
- A crash on a channel declared inside a struct.
- A missing
unsigned:Nbitfield type. priority— the one that actually matters. SpinS treats a proctype’sprioritydeclaration as a simulation-only hint, which was Spin’s semantics before version 6.2.0. Since 6.2.0,prioritygenuinely restricts which interleavings even native Spin’s own exhaustive search considers — confirmed directly in Spin’s own source (run.c’spc_highest()) — and this is the false-positive deadlock referenced above: removingpriorityfrom the affected model uncovered a previously-hidden real deadlock thatpriorityhad been silently masking. SpinS drops the restriction entirely and explores every interleavingprioritywas meant to exclude, with no warning that anything was skipped. Scope this fix to static per-proctype declarations.
Bonus: Any additional discrepancy fixed.
Deliverable
- A reproducible build of LTSmin + SpinS, with native Spin as the verification oracle, and the three fixes in-tree.
- The conformance test suite itself: infrastructure that runs a model through both tools and diffs verdicts, plus its curated corpus.
- The final report.
Requirement
- Proficiency in Java (SpinS’s implementation language) and comfort reading unfamiliar compiler internals.
- Basic familiarity with model checkers and automata/transition systems.
What you will learn
Real engineering practice: safely extending a large, unfamiliar codebase (~30K lines), building verification infrastructure, and validating correctness empirically rather than by inspection — plus the GitHub collaboration workflow (issues, PRs, code review) and hands-on contribution to an open-source project.
Take-home questions
- Staying in sync: SpinS drifted from Spin’s actual semantics because nothing kept it in sync with upstream after 2018 — the
prioritygap sat undetected for years. Once this bridge is repaired, how should it avoid the same fate? Is automated differential testing against future Spin releases (e.g. in CI) a realistic answer, or would a different architecture be better long-term — refactoring Spin’s own source to expose its parser as a reusable, decoupled component, and rebuilding SpinS on top of that shared parser instead of maintaining an independent reimplementation?