Promela: Modellierungssprache für den Model Checker SPIN

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+.