# HG changeset patch # User Eugen Sawin # Date 1311631012 -7200 # Node ID 06075f73ff125c698074013f3836fee7a6c5447d # Parent 9938ea8ed067a08706ea6c78bf7490a8c861cebf Some more notes. diff -r 9938ea8ed067 -r 06075f73ff12 slides/notes.txt --- a/slides/notes.txt Fri Jul 22 23:39:42 2011 +0200 +++ b/slides/notes.txt Mon Jul 25 23:56:52 2011 +0200 @@ -1,15 +1,13 @@ -Guten Morgen! Mein Name ist Eugen Sawin und ich werde jetzt den einführenden Vortrag halten zum Seminar Automatenkonstruktionen im Model Checking. +Guten Morgen! Mein Name ist Eugen Sawin und ich werde den einführenden Vortrag halten zum Seminar Automatenkonstruktionen im Model Checking. -Was ich ihnen erzählen werde, wird die Meisten von euch bei der Bearbeitung des Themas in irgendeiner Form tangiert haben. - -Meine Präsentation soll einen Überblick geben über die algorithmische Verifikation reaktiver Systeme basierend auf dem automaten-theoretischen Ansatz des Model Checkings. +Meine Präsentation soll einen Überblick über die algorithmische Verifikation reaktiver Systeme basierend auf dem automaten-theoretischen Ansatz des Model Checkings geben. ==> 2 -PHI ist erfüllt im Modell M, oder Modell M modelliert PHI. +Modell M erfüllt PHI. Das ist der Kern unserer Bemühungen. Doch was bedeutet das? -Wir übersetzen das in die Problemstellung der Verifikation von Systemen. +Wir übersetzen das in die Problemstellung der Verifikation. ==> 3 @@ -29,6 +27,10 @@ Die Industrie investiert viel Zeit und Geld in die Verifikation sicherheitskritischer Systeme und der Kernkomponenten anderer Systeme. Die automatisierte Verifikation hat bereits in der Chip-Verifikation ihre praktische Anwendbarkeit gezeigt und ist in der Softwareindustrie stark gefragt. +==> 4(2) + +Hier sind einige promitente Vertreter der Industry, die Verifikationsmethoden einsetzten. + Also fangen wir an. ==> 5 @@ -67,6 +69,14 @@ Die Erweiterung sind das kalligraphische X, welches für "Next" steht und das "Until" aus dem Beispiel. Diese Syntaxdefinition bildet das Fundament für weitere abgeleitete Verknüpfungen. +==> 7(2) + +Schauen wir diese kurz an. +Eine klassische Ableitung für "Wahr" bietet sich durch p oder nicht p an. +Andere Ableitungen folgen analog. +Interessant sind hierbei wieder die modalen Verknüpfungen, Diamand und Box. +Diamant steht für eine Eventualität und Box steht für eine Notwendigkeit. + ==> 8 Wir interpretieren LTL-Formeln über unendliche Sequenzen von Aussagen. @@ -134,7 +144,8 @@ Halten wir das Ganze formal fest. Wenn ich von Automaten spreche, meine ich im allgemeinen nicht-deterministische Büchi-Automaten. -Diese bestehen aus : - einem endlichen Alphabet, in unserem Beispiel war das die Menge {a,b}. +Diese bestehen aus: +- einem endlichen Alphabet, in unserem Beispiel war das die Menge {a,b}. - einer endlichen Menge von Zuständen - einer Menge von Startzuständen, in unserem Beispiel war das lediglich der Zustand q0 - der Übergangsrelation Delta @@ -169,7 +180,22 @@ ==> 19 Wir kennen nun die Sprache zur Spezifikation von Systemeigenschaften und wir haben Automaten kennengelernt, die auf unendlichen Eingaben arbeiten. +Für die automaten-theoretische Methode müssen einen Automaten konstruieren anhand einer Systemspezifikation in der linearen temporalen Logik. +In meiner Arbeit geschieht dies über den sog. Fischer-Ladner-Abschluss. +In der Arbeit von Rob Gerth wird eine on-the-fly Konstruktion der Produktautomaten vorgestellt. +Darauf wird Christian Schilling heute Nachmittag genauer eingehen. + +==> 20 + +==> 21 + +==> 22 + Erinnern wir uns and die Problembeschreibung vom Anfang. +Übersetzt in die Automatentheorie bedeutet das: +Ein System entspricht der Spezifikation, wenn die akzeptierte Sprache des Systemautomaten in der akzeptierten Sprache des Formelautomaten enthalten ist. +Eine mengentheoretische Umformung gibt uns folgende Form: +Ein System entspricht der Spezifikation, wenn der Schnitt der akzeptierten Sprache des Systemautomaten mit der akzeptierten Sprache des Automaten für die negierte Formel gleich der leeren Menge ist.