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.

Die Z-Notation (gesprochen „Zed") ist eine formale Spezifikationssprache, die Jean-Raymond Abrial ab den 1970er-Jahren an der Universität Oxford entwickelte. Sie basiert auf der Zermelo-Fraenkel-Mengenlehre und der Prädikatenlogik — daher der Name — und ist seit 2002 als ISO-Standard 13568 genormt. Mit Z beschreibt man den Zustand eines Systems und seine Operationen präzise, ohne sofort implementieren zu müssen.

Schema-Boxen

Konto
────────────────────────
kontostand : Z
────────────────────────
kontostand >= 0

Eine Schema-Box hat einen Namen, einen Deklarationsteil (Variablen mit Typen) und einen Prädikatenteil (Invarianten). Operationen beschreibt man als Schemata mit Δ (Zustand ändert sich) oder Ξ (Zustand bleibt unverändert):

Einzahlen
────────────────────────
ΔKonto
betrag : Z
────────────────────────
betrag > 0
kontostand' = kontostand + betrag

Der Apostroph (') bezeichnet den Variablenwert nach der Operation — dasselbe Muster wie in TLA+.

Mathematische Bausteine

• Mengen und Relationen: ∈, ⊆, ∪, ∩, , ×.
• Funktionen: totale Funktion →, partielle Funktion ⇸, Maplet ↦.
• Sequenzen: seq, Länge #, Verkettung ^, head/tail.
• Domäne/Range: dom, ran.

Werkzeuge und Einsatz

Werkzeuge sind fuzz (Spivey), Z/EVES, ProofPower-Z und das Open-Source-Framework Community Z Tools (CZT) mit Parser, Typchecker und LaTeX-/Unicode-Ausgabe. Z wurde unter anderem bei der Mondex-Smartcard-Geldbörse und im IBM-CICS-Umfeld eingesetzt. Während Z Struktur und Zustand mathematisch spezifiziert, modellieren Promela mit dem Model Checker SPIN ausführbares Prozessverhalten; Beweisassistenten wie Isabelle verifizieren die so aufgeschriebenen Eigenschaften maschinell.

Promela (Process oder Protocol Meta Language) ist eine Modellierungssprache für nebenläufige und verteilte Systeme, entwickelt von Gerard J. Holzmann in den Bell Laboratories. Mit Promela beschreibt man das Verhalten von Prozessen und ihre Kommunikation abstrakt — nicht als ausführbares Programm, sondern als Modell, das der Model Checker SPIN systematisch auf Fehler untersucht.

Grundbausteine

mtype = { request, reply }
chan link = [1] of { mtype }

proctype Sender(chan out) {
  do
    :: out!request
  od
}

proctype Empfaenger(chan in) {
  byte msg;
  in?msg;
  printf("erhalten: %d
", msg)
}

init {
  run Sender(link);
  run Empfaenger(link)
}

• proctype deklariert einen Prozesstyp; run startet Instanzen.
• mtype definiert benannte symbolische Konstanten.
• chan deklariert einen Kanal; ! sendet, ? empfängt. Kanäle mit Länge 1 puffern eine Nachricht, mit Länge 0 arbeiten sie als Rendezvous (Synchronisation).
• Datentypen: bit, bool, byte, int.
• atomic { ... } und d_step { ... } fassen Anweisungen zu unteilbaren Schritten zusammen.
• do ... od ist die Schleife, if ... fi die bedingte Auswahl — beide mit Wächtern (::).

Eigenschaften prüfen

Neben assert-Aussagen formuliert man zeitliche Anforderungen in Linearer Temporaler Logik (LTL): [] (immer), <> (schließlich), -> (impliziert), U (until). Ein never claim beschreibt das Verhalten, das niemals eintreten darf; SPIN erzeugt daraus automatisch den Prüfautomaten.

Die Verifikation eines Protokolls läuft typischerweise als spin -a modell.pml, gefolgt vom Kompilieren des erzeugten pan.c — Details im Artikel SPIN: Model Checker. Wer Systeme spezifizieren will, ohne die Model-Checking-Toolkette aufzubauen, verwendet die mathematische Z-Notation; für zeitliches Verhalten auf höherer Abstraktionsebene gibt es TLA+.

Nial (Nested Interactive Array Language) ist eine funktionale Array-Programmiersprache, die von Mike Jenkins und Trenchard More ab 1979 an der Queen's University at Kingston zusammen mit dem IBM Cambridge Scientific Center entwickelt wurde. Nial macht verschachtelte Arrays (nested arrays) zum zentralen Datentyp: Anders als klassische Array-Sprachen wie APL erlaubt Nial Arrays, deren Elemente selbst wieder Arrays verschiedener Form sein können.

Grundkonzepte

• Atome: Zahlen, Zeichen und Wahrheitswerte (Atom = Array der Tiefe 0)
• Arrays: rechteckige (rectilinear) Sammlungen von Atomen oder Arrays, z. B. 1 2 3 oder [1 2 3; 4 5 6]
• Operatoren: werden per first, rest, link etc. direkt auf Arrays angewendet
• Transformers: höherstufige Operatoren wie EACH, REDUCE, FORK oder ITERATE kombinieren und steuern Operationen

Wichtige Befehle

first 1 2 3        # 1 (erstes Element)
rest 1 2 3         # 2 3 (Rest ohne erstes Element)
last 1 2 3         # 3
link 1 2 3 4 5     # verkettet Arrays zu einem
count 1 2 3        # 3 (Anzahl der Elemente)
pick [2; 1 2 3]    # gezielter Zugriff auf ein Element
drop 2 1 2 3       # 3 (ohne die ersten zwei Elemente)
find 2 1 2 3       # 2 (Position des Elements)

Weitere häufige Operatoren sind front, cull, cut, grid, mix, laminate, cart, pack, gradeup, random sowie die mathematischen plus, minus, product, quotient, power, mod, max, min, abs, ceiling und floor. Prädikate wie atomic, depth, empty, equal, in, match, isinteger und ischar prüfen Eigenschaften von Werten.

Q'Nial

Die portable Implementierung Q'Nial (Jenkins, Software – Practice and Experience 1989) läuft auf Unix, Windows und macOS und bringt eine interaktive Umgebung mit. Nial war einflussreich für die Forschung an verschachtelten Array-Modellen und wird bis heute gepflegt (aktuelle Versionen unter nial-array-language.org).

Verwandte Grundlagen: APL-Befehle, J-Befehle, Ivy-Befehle, BQN-Befehle.