Veranstaltung

Nachweis:

Die Erfolgskontrolle wird in der Modulbschreibung erläutert.

Lerninhalt:

Methoden für die formale Spezifikation und Verifikation - zumeist auf der Basis von Logik und Deduktion - haben einen hohen Entwicklungsstand erreicht. Es ist zu erwarten, dass sie zukünftig traditionelle Softwareentwicklungsmethoden ergänzen und teilweise ersetzen werden.

Nahezu sämtliche formale Spezifikations- und Verifikationsverfahren haben zwar die gleichen theoretisch-logischen Grundlagen, wie man sie etwa in der Vorlesung "Formale Systeme" kennenlernt. Zum erfolgreichen praktischen Einsatz müssen die Verfahren aber auf die jeweiligen Anwendungen und deren charakteristischen Eigenschaften abgestimmt sein. An die Anwendung angepasst sein müssen dabei sowohl die zur Spezifikation verwendeten Sprachen als auch die zur Verifikation verwendeten Kalküle.

Auch stellt sich bei der praktischen Anwendung die Frage nach der Skalierbarkeit, Effizienz und Benutzbarkeit (Usability) der Verfahren und Werkzeuge.

In der Lehrveranstaltung werden eine Reihe von typischen Spezifikations- und Verifikationsmethoden und -werkzeugen und die für sie jeweils typischen Anwendungsszenarien vorgestellt. Die den Methoden zugrundeliegenden theoretischen Konzepte werden vorgestellt. Ein wesentliches Element der Lehrveranstaltung ist, dass die Studierenden mit Hilfe kleiner Anwendungsfälle lernen, die Methoden und Werkzeuge praktisch anzuwenden.

Beispiele für Methoden und Werkzeuge, die vorgestelt werden können, sind:

• Verifikation funktionaler Eigenschaften imperativer und objekt-orientierter Programme (KeY-System)

• Systemmodellierung durch Verfeinerung (Event-B mit Rodin)

• (Probabilistisches) Model Checking (SPIN und PRISM)

• Interaktives Theorembeweisen in Logiken höherer Stufe (Isabelle/HOL)

• Techniken zur statischen Analyse von Programmen (bspw. Abstrakte Interpretation)

• Beweise von Programmeigenschaften durch Typsysteme

• Software Bounded Model Checking (bspw. JJBMC)

• Spezifikation und Verifikation von Sicherheitseigenschaften (KeY, JIF)

Voraussetzungen:

---

Empfehlungen:

Es werden Grundlagenkenntnisse im Bereich Formale Systeme vorausgesetzt. Diese können entweder durch den Besuch des entsprechenden Stammoduls, oder durch das Studium des Vorlesungsskriptes angeeignet werden

Lernziele:

Die Studierenden sollen mit einer representativen Auswahl der in der formalen Programmentwicklung eingesetzten Spezifikations- und Verifikationswerkzeuge bekanntgemacht werden. Sie sollen die jeweils zugrunde liegende Theorie und die charakteristischen Eigenschaften der Methoden kennen und verstehen lernen, sowie praktische Erfahrungen mit den Werkzeugen sammeln. Am Ende der Veranstaltung sollen sie ein passendes Verifikationswerkzeug für ein gegebenes Anwendungsszenario qualifiziert auswählen können.