1 1. Guten Morgen! Mein Name ist Eugen Sawin und ich werde jetzt den einführenden Vortrag halten zum Seminar Automatenkonstruktionen im Model Checking.
3 2. Was ich ihnen erzählen werde, wird die Meisten von euch bei der Bearbeitung des Themas in irgendeiner Form tangiert haben.
5 3. Meine Präsentation soll einen Überblick geben über die algorithmische Verifikation reaktiver Systeme basierend auf dem automaten-theoretischen Ansatz des Model Checkings.
9 4. PHI ist erfüllt in Modell M, oder Modell M modelliert PHI.
10 Das ist der Kern unserer Bemühungen.
11 Doch was bedeutet das?
12 Wir übersetzen das in die Problemstellung der Verifikation von Systemen.
16 5. Gegeben sei ein Programm und dessen Spezifikation, das Problem lautet:
17 erfüllt jeder Durchlauf des Programms die Spezifikation?
19 Bevor wir an die Tat schreiten um das Problem zu lösen,
20 möchte ich eine andere Frage beantworten.
22 Wieso das Ganze? Was ist der praktische Nutzen der Verifikation?
26 Hard- und Softwaresysteme haben alle Bereiche der Industrie und damit auch unseren Alltag durchdrungen.
27 Sie bilden die Infrastruktur unserer Kommunikation, bieten Sicherheit und retten sogar Leben.
28 Und sie werden immer komplexer.
29 Die Industrie investiert viel Zeit und Geld in die Verifikation sicherheitskritischer Systeme und der Kernkomponenten anderer Systeme.
30 Die automatisierte Verifikation hat bereits in der Chip-Verifikation ihre praktische Anwendbarkeit gezeigt und ist in der Softwareindustrie stark gefragt.
36 Wenn ich sage: "Es ist dunkel." ist es nicht eindeutig, was ich damit ausdrücken möchte.
38 Ich könnte damit meinen "Es ist immer dunkel.", doch das spricht gegen unsere Intuition.
39 Wir denken als Erstes eher an "Es ist im Moment dunkel.", was auch stimmt, wenn ich damit die Folien referenziere (oder das Wetter draußen).
41 Wenn wir nach draußen schauen, können wir aus Erfahrung behaupten, dass es "notwendigerweise irgendwann dunkel wird."
43 Unsere Sprache erlaubt es uns auch kausale Zusammenhänge zu bilden, wie z.B. "Es ist dunkel, bis Jemand das Licht an macht."
45 Wir sehen, dass die natürliche Sprache nicht eindeutig ist und somit zur formalen Beschreibung ungeeignet.
46 Wie können wir unsere Sprache zähmen, ohne die Ausdruckskraft zu verlieren.
47 Nun, als Ersten machen wir das Licht wieder an!
51 Nehmen wir den letzten Satz in einer allgemeineren Form als Beispiel.
52 Dieser Satz sollte allgemeingültig sein.
53 Wie können wir die Aussage dieses Satzes formal festhalten?
54 Wir bedienen uns der Aussagenlogik und erweitern diese um eine weitere Verknüpfung.
58 Dabei sind p0 und p1 Elementaraussagen, sog. Atome, die entsprechend für "Es is dunkel" und "Es gibt licht" stehen.
59 Die neue Verknüpfung nennen wir trivialerweise "until" und notieren sie mit dem kalligraphischen U.
60 Halten wir das formal fest.
64 Wir definieren die Syntax der linearen temporalen Logik mit Hilfe dieser Produktionen in Backus-Naur-Form.
65 Somit ist eine LTL-Formel entweder ein aussagenlogisches Atom, eine negierte Formel oder eine Disjunktion zweier Formeln.
66 Das kannten wir bereits aus der Aussagenlogik.
67 Die Erweiterung sind das kalligraphische X, welches für "Next" steht und das "Until" aus dem Beispiel.
68 Diese Syntaxdefinition bildet das Fundament für weitere abgeleitete Verknüpfungen.
72 Wir interpretieren LTL-Formeln über unendliche Sequenzen von Aussagen.
73 Die Sequenz entspricht der zeitlichen Abfolge von Ereignissen in einem vorwärts gerichteteten diskreten Zeitverlauf.
74 Diese Interpretation heißt die Kripke-Semantik.
75 Das Kripke-Modell der LTL-Semantik besteht aus einer abzählbaren Menge von Zuständen, verknüpft duch die Erreichbarkeitsrelation und der Bewertungsfunktion V.
76 Da wir nur lineare Abfolgen betrachten, fällt die Erreichbarkeitsrelation einfach aus.
77 Von einem beliebigen Zustand ist jeweils nur dessen Nachfolger erreichbar.
78 Die Bewertungsfunktion liefert uns die Menge aller gültigen Atome für einen bestimmten Zustand.
79 Intuitiv sagt man, ein Atom p ist wahr zum Zeitpunkt i gdw. p in der Menge V(i) ist.
83 Hier ist eine Veranschaulichung eines Beispielmodells.
84 Man sieht die Zustände s0 bis si und den Zeitverlauf durch die Relation R.
85 Für jeden Zustand ist die Rückgabe der Bewertungsfunktion als Menge positiver Atome abgebildet.
89 Die Erfüllbarkeit einer Formel zu einem Zeitpunkt i im Modell M ist folgendermaßen definiert:
90 - ein Atom p ist erfüllbar gdw. und p in der Menge V(i) ist
91 - eine negierte Formel PHI ist erfüllbar gdw. PHI nicht erfüllbar ist
92 - eine Disjunktion von PHI und PSI ist erfüllbar gdw. PHI oder PSI erfüllbar ist
93 - Next PHI ist erfüllbar gdw. PHI im darauffolgenden Zeitpunkt erfüllbar ist
94 - PHI Until PSI ist erfüllbar gdw. es einen Zeitpunkt k gibt, ab dem PSI erfüllbar ist und für alle Zeitpunkte vor k PHI erfüllbar ist.
96 Mit Hilfe der linearen temporalen Logik lassen sich Programmeigenschaften und derren zeitliche Abhängigkeiten genau beschreiben.
97 Als nächstes werden wir uns den Automaten widmen, die auf unendlichen Eingaben operieren.
101 Wieso sind unsere Eingaben überhaupt unendlich?
102 Im Gegensatz zu terminierenden Programmen sind reaktive Systeme fortlaufende Prozesse.
103 Ein mal initiiert, verbleiben reaktive Systeme in einem aktiven Zustand und reagieren auf nebenläufige Eingaben.
104 Theoretisch betrachtet, arbeiten solche Systeme somit auf unendlichen Eingabesequenzen.
108 Hier ist ein Beispielautomat, der auf unendlichem Input arbeitet.
109 Sieht jemand auf Anhieb welche Sprache dieser Automate akzeptiert?
110 w1 ist eine Eingabe, der Überstrich soll eine periodische Wiederholung der Sequenz darstellen.