Model Checking
Model Checking überprüft erschöpfend, ob alle Zustände eines Systems temporallogische Eigenschaften erfüllen, und findet automatisch Gegenbeispiel-Zustände, die sie verletzen.
Zweck
Erschöpfende Verifikation von Sicherheit und Lebendigkeit nebenläufiger Systeme, automatisches Auffinden von Deadlocks und Datenrennen.
Mechanismus
Das System wird als Zustandsmaschine modelliert und Eigenschaften in Temporallogik (LTL/CTL) ausgedrückt. Explizite Zustandsaufzählung oder symbolische BDDs durchlaufen alle Zustände. Schlägt eine Eigenschaft fehl, wird ein Gegenbeispiel-Pfad erzeugt. SPIN und NuSMV sind gängige Werkzeuge.
Anwendungsfälle
- Verifikation von Nebenläufigkeit
- Protokollverifikation
- Hardware-Verifikation