Erlernt werden sollen Methoden der Systemverifikation, wie Model Checking, 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, Statecharts, Petrinetzen und Prozessalgebra. Spezielle Methoden sind Binäre Entscheidungsdiagramme (BDDs), symbolische und parametrisierte Methoden, sleep-set- und stubborn-set-Methoden, Reduktionen durch partielle Ordnungen, Symmetrieausnutzung, Verifikation von Sicherheits-, Lebendigkeits und Fairness-Eigenschaften, strukturelle Methoden, deduktive- und prozessalgebra-basierte Methoden | |
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. 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 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. | |
Hauptstudium, Vertiefungsgebiete P1, P2, P4, P5, Th1, Th2, Th3, Th4; Schwerpunkte BV, ES, IM, INE, OSE, RNT, SEM, SV, VIS, WV | |
Grundstudium | |
Vorlesung mit gelegentlichen Übungen | |
| |
unregelmäßig | |
Geeignet für Bioinformatikstudierende, Wirtschaftsinformatikstudierende. Bedingt geeignet für Lehramtsstudierende, Nebenfachstudierende. | |
Petrinetze, Verifikation, Model Checking, temporale Logik, Symmetrie, BDDs, strukturelle Methoden, sleep-set-Methode, stubborn-set-Methode |