Spezifikation und Verifikation: Infinite State Systems.
Analyse von Systemen mit unendlichem Zustandsraum.

Veranstalter: Michael Köhler-Bußmeier
Termin: Donnerstag, 8:30-10:00 in C-221 (im Sommer 2008)

Die Vorlesung Spezifikation und Verifikation unterteilt sich in die Veranstaltung Model-Checking am Montag und Infinite State Systems am Donnerstag. Beide Teile sind jeweils in sich abgeschlossen, so dass Studierende des Diplomstudiengangs wahlweise auch nur eine der beiden Veranstaltung besuchen können.

Vorgehen und Inhalt

Zur Einführung werden entsprechende Teile aus FGI-2/PNL und FGI-3/LOS kurz wiederholt. Daran schließen sich weitere und vertiefende Inhalte an Hierbei wird - dem Charakter einer kleineren Vorlesung entsprechend - auf die speziellen Wünsche und Bedürfnisse der Teilnehmenden eingegangen.

Aus dem KVV: Systeme, die keinen endlichen Zustandsraum besitzen, können nicht mehr durch Model-Checking verifiziert werden. Trotzdem ist es möglich, diese Systeme zu analysieren: Das Erreichbarkeitsproblem für unbeschränkte Petrinetze ist ein berühmtes Beispiel für ein entscheidbares Problem. Die Analyse solcher Systeme weist Bezüge zum Theorembeweisen und damit auch zu funktionalen Programmiersprachen, zum Lamdakalkül und zu Logiken höherer Ordnung auf. Typische Anwendungsgebiete sind mobile Systeme, kryptografische Protokolle und eingebettete Systeme.

Literatur:

Materialien zur Veranstaltung

Korrekturen und Anmerkungen bitte an Michael Köhler-Bußmeier.

>  [Lehre] [TGI] [Informatik]  <

Impressum