SPIN: Model Checker für Promela-Modelle

SPIN (Simple Promela Interpreter) ist ein Model Checker von Gerard J. Holzmann, der seit den 1980er-Jahren in den Bell Laboratories entwickelt wurde und heute als freie Software auf spinroot.com verfügbar ist. SPIN liest ein Modell in Promela und durchsucht dessen Zustandsraum automatisch nach Fehlern wie Deadlocks, verletzten Assertions oder unerwünschten Endzuständen.

Typischer Verifikations-Workflow

spin -a modell.pml      # erzeugt pan.c (Verifier)
gcc -o pan pan.c        # kompiliert den Verifier
./pan -m100000          # Tiefensuche mit maximaler Tiefe
./pan -a                # Assertion-Verletzungen prüfen
./pan -l                # LTL-Eigenschaften (never claims) prüfen

Meldet der Verifier einen Fehler, legt SPIN eine .trail-Datei an. Mit spin -t -p -g modell.pml spielt man den Gegenbeispiel-Pfad schrittweise ab und sieht, welche Prozesse in welcher Reihenfolge welche Aktionen ausführen.

Suchmodi und Eigenschaften

  • Exhaustive Suche: vollständige Tiefensuche über alle erreichbaren Zustände — vollständig, aber speicherhungrig.
  • Bitstate-Hashing (Supermode): approximative Suche mit komprimierter Zustandsablegung; findet Fehler zuverlässig, kann aber Zustände überspringen.
  • LTL: spin -f "[] (p -> <> q)" übersetzt eine Formel in einen never claim, der während der Suche überwacht wird.
  • Lebendigkeit: Akzeptanz- und Non-Progress-Zyklen decken Livelocks auf.
  • Fairness: schwache/starke Fairness-Annahmen verhindern künstliche Gegenbeispiele durch verhungernde Prozesse.

Oberflächen und Einsatz

iSpin (Tcl/Tk) und jSpin (Java) sind grafische Oberflächen; in CI-Umgebungen läuft SPIN rein über die Kommandozeile. Eingesetzt wird SPIN seit Jahrzehnten zur Verifikation von Kommunikationsprotokollen, Bahnsteuerungen und eingebetteten Systemen. Verwandte formale Ansätze: TLA+ mit seinem Model Checker TLC und die mengentheoretische Spezifikationssprache Z-Notation.