Model-Checking
» This course is given in German.
Vorlesung im Sommersemester 1999
| Art | Termine/Ort | Beginn | Veranstalter |
|---|---|---|---|
| V2 | Mi 08:15 - 09:45 5052 | 21.04.1999 | Wilke |
| Ü2 | Mi 16:15 - 17:45 5052 | Wilke |
Inhalt
Unter einem Model-Checker versteht man Software, mit deren Hilfe man (vollautomatisch) überprüfen kann, ob ein gegebenes System (Hardware-Baustein, Kommunikationsprotokoll, Steuerungseinheit, etc.) eine vorgegebene gewünschte Eigenschaft besitzt bzw. inwiefern es sie verletzt. Dabei wird die Eigenschaft meistens in einer sogenannten Spezifikationslogik formalisiert und das gegebene System auf eine geeignete Weise als Transitionssystem (im weiteren Sinne) modelliert.
In der Vorlesung werden die gebräuchlichen Spezifikationslogiken (wie z.B. CTL, LTL, Mü-Kalkül) vorgestellt, Algorithmen für die entsprechenden Model-Checking-Probleme entwickelt (in Abhängigkeit von der Darstellung der Transitionssysteme) und obere und untere Schranken für deren Komplexität hergeleitet.
Übung: In den Übungen wird der Stoff der Vorlesung vertieft und darüber hinaus werden einige Model-Checker (wie z.B. SMV) vorgestellt werden.
Zuordnung
Theoretische Informatik, Informatik Vertiefung
Voraussetzungen
Grundlagen in Automatentheorie und mathematischer Logik erwünscht