Grundlagen der formalen Methoden

In einem Spiel können zwei Spieler im selben Augenblick das letzte Ticket greifen. Du testest tausendmal, und es klappt. Der Fehler braucht eine ganz bestimmte Reihenfolge von Ereignissen und zeigt sich beim tausendundersten Mal. Eine formale Methode probiert keine Fälle aus. Sie lässt eine Maschine alle ansehen.

• Eigenschaft: eine Aussage über ein System, die immer wahr sein soll.
• Solver: ein Programm, das Werte findet, die zu Regeln passen.
• Modellprüfer: ein Programm, das alle Zustände durchprobiert, die ein Modell erreichen kann.
• Invariante: eine Eigenschaft, die in jedem Zustand gelten muss.
• Gegenbeispiel: ein Ablauf, der zeigt, dass die Eigenschaft falsch ist.
• Modell: eine kleine Beschreibung eines Systems, die Einzelheiten weglässt.

Z3 ist ein Solver. Du gibst ihm Regeln, und er antwortet sat (erfüllbar: es gibt passende Werte) mit einem Beispiel oder unsat (kein Wert passt). Der erste Befehl zeigt die Version. Der zweite fragt nach einer Zahl x über 3 und unter 6: Z3 sagt sat und gibt für x die 4. Der dritte fragt nach einer Zahl über 5 und unter 3: Z3 sagt unsat. So beweist es: Um eine Behauptung zu beweisen, frage nach einem Fall, in dem sie scheitert, und erhalte unsat.

SPIN prüft Modelle, die in Promela geschrieben sind. Dein Lab hat eines: Zwei Arbeiter addieren 1 zu einem gemeinsamen Zähler, mit einem Lock, das noch nichts tut. spinrun baut den Prüfer und lässt ihn über alle Reihenfolgen laufen, die die Arbeiter nehmen können. Er gibt assertion violated (inside==1) und errors: 1 aus und behält einen Ablauf. Der zweite Befehl spielt diesen Ablauf Schritt für Schritt ab: Beide Arbeiter haben inside = (inside+1) ausgeführt, bevor einer wieder draußen war.

TLA+ beschreibt ein System als Zustände und Schritte, und TLC prüft es. Die Lock.tla des Labs hat zwei Prozesse, die jeweils idle, wait oder cs (im kritischen Abschnitt) sein können. Diese Invariante sagt, dass nie beide warten. Das ist selbst für ein korrektes Lock falsch: TLC gibt Invariant NotBothWaiting is violated und ein Gegenbeispiel aus drei Zuständen aus, das damit endet, dass beide Prozesse bei wait stehen. Die eigentliche Aufgabe des Labs ist eine andere Invariante.

Alloy beschreibt Dinge und die Verbindungen zwischen ihnen und sucht dann ein kleines Beispiel, das eine Behauptung bricht. Hier sind die Dinge Personen und wer mit wem befreundet ist. alloy führt beide Befehle der Datei aus. check Symmetric gibt SAT aus: Alloy hat ein Gegenbeispiel gefunden, zwei Personen, von denen die eine die andere als Freundin zählt und nicht umgekehrt, dargestellt als Person$1->Person$0. run Meet gibt ebenfalls SAT aus: Es hat ein Beispiel zum Ansehen gefunden. Bei einem check heißt SAT, dass die Behauptung falsch ist.