| Veranstaltungs-Nr.: | 18.215 (WiSe 2004/2005) |
| Titel: | Verifikation von Systemmodellen |
| Veranstalter: | Daniel Moldt, Rüdiger Valk |
| Zeit / Ort: | 2 st. Mo. 10-12 C-221 |
| - |
| Inhalt: | 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.
Zur Vertiefung der Modellierung wird auf die Veranstaltung 18.213 "Modellbildung mittels semiformaler und formaler Techniken" hingewiesen. |
| Lernziel: | 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 |
| Stell. im Studienplan: | Hauptstudium; Schwerpunkte OSE, IM, RNT, SV, BV, SEM, INE, ES, WV, VIS |
| Voraussetzungen: | Grundstudium |
| Vorgehen: | Vorlesung mit gelegentlichen Übungen |
| Literatur: | - C. Girault, R. Valk: Petri Nets for Systems Engineering , Springer, Berlin, 2003, Part III: Verification
- E.M. Clarke et al.: Model Checking, The MIT Press, Cambridge, 1999
- B. Bérard et al.: Systems and Software Verification, Springer, Berlin, 1999
|
| Periodizität: | unregelmäßig |
| Eignung: | Geeignet für Bioinformatikstudierende, Wirtschaftsinformatikstudierende. Bedingt geeignet für Lehramtsstudierende, Nebenfachstudierende. |
| Stichworte: | Model Checking, temporale Logik, Symmetrie, BDDs, strukturelle Methoden, sleep-set-Methode, stubborn-set-Methode, Petrinetze, Verifikation |