inf408 - Algorithmen zur Software-Verifikation (Vollständige Modulbeschreibung)

inf408 - Algorithmen zur Software-Verifikation (Vollständige Modulbeschreibung)

Originalfassung Englisch PDF Download
Modulbezeichnung Algorithmen zur Software-Verifikation
Modulkürzel inf408
Kreditpunkte 6.0 KP
Workload 180 h
Einrichtungsverzeichnis Department für Informatik
Verwendbarkeit des Moduls
  • Master of Education (Gymnasium) Informatik (Master of Education) > Wahlpflichtmodule (Theoretische Informatik)
  • Zwei-Fächer-Bachelor Informatik (Bachelor) > Wahlpflicht Theoretische Informatik (30 KP)
Zuständige Personen
  • Olderog, Ernst-Rüdiger (Modulverantwortung)
  • Lehrenden, Die im Modul (Prüfungsberechtigt)
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:
  • führen CTL-Model-Checking an Beispielen durch
  • konstruieren abstrakte Kripke-Strukturen an Hand vorgegebener Datenabstraktionen und führen an Beispielen Abstraktions-Verfeinerungs-Schleifen durch
  • charakterisieren die Konzepte der Simulation und Bisimulation
  • verstehen das Konzept der Abstraktion von Daten und Transitionen
  • beschreiben Model-Checking-Verfahren als Instanzen von Fixpunkt-Algorithmen


Methodenkompetenzen
Die Studierenden:
  • spezifizieren reaktive Systeme mit Hilfe von Kripke-Strukturen und CTL-Formeln
  • setzen Model-Checking-Verfahren in praktische Algorithmen (in Java) um


Sozialkompetenzen
Die Studierenden:
  • arbeiten in Kleingruppen


Selbstkompetenzen
Die Studierenden:
  • reflektieren ihr eigenes Handeln und beziehen dabei die vorgestellten Methoden ein
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
  • E.M. Clarke, O. Grumberg, and D. Peled: Model Checking. MIT Press, 2000.
  • F. Nielson, H.R. Nielson, and C. Hankin: Principles of Program Analysis, Springer, 2005
  • E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-guided abstraction refinement for symbolic model checking, Journal of the ACM 50(5) 752-794 (2003)
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