Model-Checking

aus Wikipedia, der freien Enzyklopädie

Du hast neue Nachrichten auf deiner Diskussionsseite.

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 $M \models p$ ) ?

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.

Inhaltsverzeichnis

1 Prinzip
2 Temporallogische Formeln
3 Typen von Model-Checking-Algorithmen
- 3.1 Explizites Model-Checking
- 3.2 Symbolisches Model-Checking
4 Praktischer Einsatz
5 Weblinks
6 Literatur

[Bearbeiten] 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.

[Bearbeiten] Temporallogische Formeln

Bei der logischen Formel, der formalisierten Spezifikation, handelt es sich oft um eine Formel einer temporalen Logik. Solche Formeln lassen sich zum Beispiel im modalen μ-Kalkül ausdrücken. Hierbei handelt es sich um einen allgemeinen Formalismus der unter anderem mit Fixpunktoperatoren auf Zustandsmengen arbeitet. Die im Model-Checking Kontext häufig benutzten Logiken CTL*, CTL und LTL sind von ihrer Ausdruckskraft im μ-Kalkül enthalten.

Im spezielleren Fall verwendet man daher CTL*, allerdings ist diese Logik auch noch zu komplex, um sich gut für Model-Checking zu eignen. Daher verwendet man oft nur eine Teilmenge dieser Logik, in der Regel LTL oder CTL. Dabei kann das Problem bestehen, die Spezifikation in der gewählten Teilmenge überhaupt ausdrücken zu können.

[Bearbeiten] Typen von Model-Checking-Algorithmen

Die Algorithmen für Model-Checking werden unterschieden in zwei Typen.

[Bearbeiten] 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-Formeln werden an den Zuständen schrittweise Teilformeln auf ihre Wahrheitswerte überprüft. Der Zustandsraumexplosion kann z.B. durch Ausnutzen von Symmetrien und Partial Order Reduction entgegengewirkt werden, um möglichst große Transitionssysteme verifizieren zu können.

[Bearbeiten] Symbolisches Model-Checking

Symbolische Model-Checker basieren entweder auf Binary Decision Diagrams (z.B. für CTL-Formeln) oder auf SAT-Solvern (z.B. 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.

[Bearbeiten] 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.