Model-Checking ist ein Verfahren zur vollautomatischen Verifikation von Systembeschreibungen (Modell) gegen eine Spezifikation (Formel). Der Begriff ist motiviert durch die mathematische Formulierung des Problems: Für eine gegebene (logische) Systembeschreibung M und eine gegebene (logische) Formel p, ist M Modell für p (formal ) ?
Das Verfahren wird als vollautomatisch bezeichnet, weil es keiner Benutzer-Interaktion bedarf (im Gegensatz zu einigen deduktiven Verfahren, wie zum Beispiel interaktives Theorembeweisen). Die Systembeschreibung erfolgt in einer formalen Sprache, zum Beispiel durch ein Programm, einen endlichen Automaten, oder durch ein Transitionssystem. Der Zustandsraum des Systems muss nicht notwendigerweise endlich, jedoch endlich repräsentierbar sein. Die Spezifikation ist die nachzuweisende formale Eigenschaft des Systems, gegeben durch eine temporallogische Formel oder durch einen Beobachtungsautomaten.
Prinzip
Eingabe des Model-Checkers ist die Systembeschreibung und die Spezifikation. Erfüllt die Systembeschreibung die Spezifikation, stoppt der Algorithmus und liefert ein Korrektheitszertifikat als Ausgabe. Findet der Algorithmus eine Verletzung der Spezifikation, stoppt der Algorithmus und liefert als Ausgabe ein Gegenbeispiel (meist ein Pfad der Systemausführung) zum Nachweis des Fehlers.
Temporallogische Formeln
Bei der logischen Formel, der formalisierten Spezifikation, handelt es sich oft um eine Formel einer temporalen Logik. Im allgemeinen Fall handelt es sich hierbei um eine Formel des modalen μ-Kalküls. Hierbei handelt sich um eine sehr allgemeine, aber auch schwer verständliche Form, die Aussagen über größte und kleinste Fixpunkte macht. Insbesondere sind die weiter unten genannten Logiken CTL*, CTL und LTL von ihrer Ausdruckskraft sogar in ihr enthalten.
Im spezielleren Fall verwendet man daher CTL*, allerdings ist diese Logik auch noch 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-Checking-Algorithmen
Die Algorithmen für Model-Checking werden unterschieden in zwei Typen.
Explizites Model-Checking
Explizites Model-Checking überprüft das Modell, indem das Transitionssystem in geeigneter Weise aufgebaut wird und mittels Graphsuche verifiziert wird. 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 der Zustandsraumexplosion entgegengewirkt, um möglichst große Transitionssysteme verifizieren zu können.
Symbolisches Model-Checking
Symbolische Model-Checker basieren entweder auf Binary Decision Diagrams (für CTL-Formeln) oder auf SAT-Solvern (für LTL-Formeln). Im ersten Fall wird je ein BDD für die Zustandsü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.
Praktischer Einsatz
Seit Anfang der 90er Jahre wurden große Fortschritte in der Performance der Algorithmen erzielt, wodurch das Verfahren für die Praxis interessant geworden ist. In der Qualitätssicherung beim Entwurf großer integrierter Schaltungen werden Model-Checker bereits in der industriellen Praxis eingesetzt. In den letzten Jahren wurden in einigen Forschungsprojekten Model-Checker für Software entwickelt.
Literatur
- Clarke, Grumberg, Peled: Model Checking. MIT Press, 2000. ISBN 0-262-03270-8