inf408 - Algorithmen zur Software-Verifikation (Veranstaltungsübersicht)

Am Ende der Vorlesungszeit

Klausur oder mündliche Prüfung

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