MIN-Fakultät
Fachbereich Informatik
Theoretische Grundlagen der Informatik
UHH > MIN > Informatik > TGI > Lehre Deutsche Version. This page is available in German only. Cette page n'existe qu'en Allemand. Ésta página sólo existe en Alemán. Web-Mail Suche Seitenende

Model Checking

Veranstalter: Rüdiger Valk

Termin: Dienstags, 12:15-13:45 in C-221 (SoSe 2012)

Dieser Modul mit dem Titel "Spezifikation und Verifikation (SuV)" unterteilt sich in die Vorlesungen "Model-Checking " am Dienstag und "Infinite State Systems" am Donnerstag. Beide Teile sind jeweils in sich abgeschlossen, so dass Studenten des Diplomstudiengangs wahlweise auch nur eine der beiden Veranstaltung besuchen können.

Motivation:

Am 4. Juni 1996 explodierte eine Ariane-5-Rakete 40 Sekunden nach dem Start. Die Untersuchungskommission stellte später als Grund eine Ausnahmebehandlung in der Flugleitsoftware fest. Eine fehlerhafte Gleit/Festkomma-Konversion verursachte im Haupt- wie im Backup-Rechner einen Fehler, der zu einer inkorrekten Datenübermittlung an den Bordrechner führte, der seinerseits daraufhin die Selbstzerstörung einleitete. Daraufhin wurde die Software einer umfangreichen Verifikation unterzogen. Model-Checking-Methoden fanden dadurch auch in Europa vermehrt Beachtung. Solche Ereignisse sind keine Einzelfälle, obwohl die Gebiete Programmierung, Softwaretechnik, Systemtechnik und verteilte Systeme in der Informatik relativ gut vertreten sind und vielfältige Methoden, Techniken und Vorgehensweisen entwickelt haben. Als Grund ist unter anderem eine unzureichende Durchdringung der genannten Gebiete mit formal abgesicherten Konzepten, Modellen und Methoden zu nennen.

In dieser Vorlesung sollen vorwiegend solche Methoden der Verifikation durch Model-Checking vorgestellt werden, die für relativ große Systeme tatsächlich angewandt werden und für die effektive Werkzeuge zur Verfügung stehen. So wurden bereits beeindruckend große Systeme erfolgreich verifiziert: beispielsweise Systeme mit mehr als 10exp20 Zuständen.

Lernziel und Vorgehen:

Erlernt werden sollen Methoden der Systemverifikation, die weitgehend unabhängig von der Systemmodellierung sind - im Gegensatz zu solchen, die spezielle Eigenschaften der Modellierung ausnutzen. Dabei sind die entsprechenden Spezifikationstechniken wie CTL, CTL*, LTL einzusetzen. Die Systemmodellierung beruht auf Zustandsdiagrammen in Form von Transitionssystemen. Spezielle Methoden oder Begriffe sind Binäre Entscheidungsdiagramme (BDDs), symbolische und parametrisierte Methoden, Reduktionen durch partielle Ordnungen, Symmetrieausnutzung, Verifikation von Sicherheits-, Lebendigkeits und Fairness-Eigenschaften, strukturelle Methoden, Methoden. Typische Anwendungsgebiete sind mobile Systeme, kryptografische Protokolle und eingebettete Systeme. Die Studenten lernen die formalen Grundlagen und erarbeiten sich ein Gefühl für die Möglichkeiten und Grenzen der formalen Spezifikation. Neben den theoretischen Grundlagen werden exemplarisch einige Computer-Werkzeuge im kleineren Rahmen praktisch vorgeführt. Typische Anwendungsgebiete sind mobile Systeme, kryptografische Protokolle und eingebettete Systeme.

Materialien zur Veranstaltung:

(Benutzername und Passwort wie bei FGI2/PNL)