inf408 - Algorithmen zur Software-Verifikation (Vollständige Modulbeschreibung)
Modulbezeichnung | Algorithmen zur Software-Verifikation |
Modulkürzel | inf408 |
Kreditpunkte | 6.0 KP |
Workload | 180 h |
Einrichtungsverzeichnis | Department für Informatik |
Verwendbarkeit des Moduls |
|
Zuständige Personen |
|
Teilnahmevoraussetzungen | |
Kompetenzziele | In der Vorlesung werden Algorithmen vorgestellt, die eine automatische Analyse und Verifikation komplexer Strukturen ermöglichen, wie sie bei Software-Systemen vorkommen. In den Übungen werden diese Algorithmen implementiert und an Fallstudien erprobt. Fachkompetenzen Die Studierenden:
Methodenkompetenzen Die Studierenden:
Sozialkompetenzen Die Studierenden:
Selbstkompetenzen Die Studierenden:
|
Modulinhalte | Software-Systeme weisen komplexe Daten- und Kontrollstrukturen sowie immer größere Zustandsräume auf, so dass sie durch Testen nur unzulänglich auf ihre Korrektheit überprüft werden können. Es ist daher ein große Herausforderung an die Informatik, automatische Methoden zur Analyse und Verifikation von Verhaltenseigenschaften für Software-System zu entwickeln. In dieser Lehrveranstaltung werden Algorithmen aus den Bereichen der Programmanalyse und des Model-Checkings vorgestellt und praktisch erprobt. Die Algorithmen verarbeiten Transitionssysteme, wie sie aus Software-Systemen entstehen, und benutzen Abstraktionstechniken für Daten und Transitionen, um die Zustandsräume analysierbar zu machen. Themen: Kripke-Strukturen, Transitionssysteme, temporale Logiken CTL und CTL*, Fixpunkt-Algorithmen für rekursive CTL-Operatoren, Model-Checking Algorithmus für CTL, Simulation und Bisimulation auf Kripke-Strukturen, Sätze über die Erhaltung von Eigenschaften bei (Bi-) Simulationen, existenzielle und universelle Abstraktion von Kripke-Strukturen, Abstraktions-Verfeinerungs-Schleife (CEGAR-Methode) |
Literaturempfehlungen |
|
Links | |
Unterrichtssprache | Deutsch |
Dauer in Semestern | 1 Semester |
Angebotsrhythmus Modul | unregelmäßig |
Aufnahmekapazität Modul | unbegrenzt |
Modulart | je nach Studiengang Pflicht oder Wahlpflicht |
Modullevel | AS (Akzentsetzung / Accentuation) |
Lehr-/Lernform | V+Ü |
Vorkenntnisse | Grundveranstaltungen in Informatik und Mathematik |
Lehrveranstaltungsform | Kommentar | SWS | Angebotsrhythmus | Workload Präsenz |
---|---|---|---|---|
Vorlesung | 2 | SoSe oder WiSe | 28 | |
Übung | 2 | SoSe oder WiSe | 28 | |
Präsenzzeit Modul insgesamt | 56 h |
Prüfung | Prüfungszeiten | Prüfungsform |
---|---|---|
Gesamtmodul | Am Ende der Vorlesungszeit |
Klausur oder mündliche Prüfung |