Model-Checking

aus Wikipedia, der freien Enzyklopädie

Du hast neue Nachrichten (Unterschied zur vorletzten Version).

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 Übersicht und Bewertung
6 Weblinks
7 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. Im allgemeinen Fall handelt es sich hierbei um eine Formel des modalen μ-Kalküls. Hierbei handelt es 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.

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

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

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

[Bearbeiten] Übersicht und Bewertung

Diese Übersicht ist eher unvollständig und sicher auch nicht sehr korrekt. Es wird dringend empfohlen das der ein oder andere "Profi" mal drüberschaut und einige Verbesserungen vornimmt.

	Installation	Dokumentation	Community	Komplexität	Erweiterbarkeit	Wird weiterentwickelt	Opensource	GUI	Windows / Linux / Mac
Uppaal	+++	+++	++	O	-	√	-	√	√/√/√
CPN – Tools	+++	+++	++	+++		√	-	√	√/√/
Blast						√	√	√	√/√/√
HyTech						-	√	-	√/√/√
FDR2						√	-		-/√/√
Kronos	++	+	O		-	-		-	√/√/
NuSMV	+++	+++			++	√		-	√/√/
SMV	--> siehe NuSMV (Weiterentwicklung) <--
Spin	+++	+++	O			√	√	-	√/√/√

-> Jspin	++					√	√	√	√/√/√
Verus			O			-	√		(√/√/√)
Model-Checking Kit	++	+	-		++	-	√	-	(√)/√/√
Raven	+++		O			-	-	√	√/√/-
									/ /
									/ /
									/ /
ESC / Java	+++					-			√/√/-
Fujaba Tool Suite	+++	+++	++		++	√	-	√	√/√/-

Stand: November 2006

Maßstab: { sehr schlecht } --- | -- | - | o | + | ++ | +++ { sehr gut } oder { niedrig } bis { hoch }
ja | vorhanden : √ ( Häkchen )
nein | nicht vorhanden: - ( Minus | Gedankenstrich )
Wird weiterentwickelt: letztes Release jünger als 2 Jahre
Blast: Eclipse-Plugin verfügbar
Model-Checking Kit: benötigt Spin