Model Checking (auch: Modellprüfverfahren) ist ein relativ neuer Ansatz zur Verifikation in der Informatik, bei dem in den letzten Jahren große Fortschritte erzielt werden konnten und der dadurch auch für die Praxis interessant geworden ist.
Im Unterschied zu anderen Verifikationstechniken, wie interaktives Theorembeweisen, handelt es sich beim Modelchecking um einen automatischen Ansatz. Seine Einsatzmöglichkeiten sind daher auf endliche System oder solche die sich auf endliche Systeme reduzieren lassen beschränkt.
Prinzip des Model Checkings
Das Model Checking läuft im Prinzip wie folgt ab. Zunächst wird aus einem System durch Abstraktion ein Modell und durch Formalisierung aus einer Spezifikation eine logische Formel gewonnen. Modell und Formel werden dann dem eigentlichen Model Checker übergeben der überprüft, ob das Modell der Spezifikation genügt. Im Idealfall wird dieser ein positives Ergebnis zurückliefern. Typischerweise liefert der Modelchecker aber entweder einen Speicherüberlauf, da das System zu komplex ist oder ein Gegenbeispiel. Im zweiten Fall liegt entweder ein Fehler im System, Modell oder der Formel vor, der korrigiert werden muss bevor Modell und Formel erneut dem Model Checker zur Verifiakton übergeben werden. Die Rückgabe eines explizten Gegenbeispiels vereinfacht die Fehlerkorrektur.
Modell
Der Model Checker verifiziert streng genommen immer ein endliches Transitionssystem, welches durchaus nichtdeterministisch sein darf. Dieses wird dem Model Checker auf Grund seiner Größe aber nicht direkt übergeben, sondern in Form einer geeigneten Sprache, zum Beispiel Guarded Commands.
Formel
Bei der logischen Formel, der formalisierten Spezifikation, handelt es sich in der Regel um eine Formel einer temporalen Logik. Im allgmeinen Fall handelt es sich hierbei um CTL*, allerdings ist diese Logik selbst zu komplex, um sich gut zur Verifikation zu eignen. Daher verwendet man oft nur eine Teilmenge dieser Logik, in der Regel LTL oder CTL. Dabei besteht natürlich das Problem, die Spezifikation in der gewählten Teilmenge überhaupt ausdrücken zu können. In der Praxis trifft dies aber auf wenigstens einen der beiden Fälle zu.
Typen von Model Checkern
Beim Model Checking unterscheidet man zwei wesentliche Typen von Model Checkern.
Explizites Model Checking
Explizite Model Checker überprüfen das Modell, indem sie das Transitionssystem in geeigneter Weise aufbauen und mittels Tiefensuche verifizieren. Bei LTL-Formeln kommen dabei Büchi-Automaten zum Einsatz, bei CTL-Formel werden an den Zuständen schrittweise Teilformeln auf ihre Wahrheitswerte überprüft. Durch ausnutzen von Symmetrien und Partial Order Reduction wird dabei versucht der Zustandsraumexplosion entgegenzuwirken, um möglichst große Transitionssysteme verifizieren zu können.
Symbolisches Model Checking
Symbolische Model Checker basieren entweder auf Binary Decision Diagram (für CTL-Formeln) oder auf SAT-Solvern (für LTL-Formeln). Im ersten Fall wird je ein BDD für die Zustansübergangsrelation und die erfüllbaren Zustände der Formel aufgebaut. Im zweiten Fall werden Modell und Spezifikation in eine aussagenlogische Formel umgewandelt, die dann auf Erfüllbarkeit überprüft wird.