| Veranstaltungs-Nr.: | 18.219 (WiSe 2005/2006) |
| 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;
Vertiefungsgebiete P5, Th3, Th2, P2, Th4, Th1, P9, P3, P4, P10;
Schwerpunkte OSE, IM, RNT, SV, BV, SEM, INE, ES, WV, VIS |
| Voraussetzungen: | Grundstudium |
| Vorgehen: | Vorlesung mit gelegentlichen Übungen |
| Verwendbarkeit: | - |
| 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: | regelmäß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 |