Modul

Siehe Teilleistung

Nach Abschluss des Moduls verfügen Studierende über folgende Kompetenzen. Sie …

• haben einen Überblick über typische in der formalen Programmentwick­lung eingesetzte Spezifikations- und Verifikationsmethoden und -werkzeuge.

• beherrschen Theori­en und Praxis der formalen Methoden und Werkzeuge, die repräsentativ in der Veranstaltung vorgestellt werden,

• können die vorgestellten Methoden und Werkzeuge erfolgreich zur Lösung praktischer Aufgaben einsetzen,

• verstehen die charakteristischen Eigenschaften der vorgestellten Methoden und Werkzeuge, können deren Vor- und Nachteile gegeneinander abwägen und können ein passendes Verifikationswerkzeug für ein gegebenes Anwendungsszenario auswählen.

Siehe Teilleistung

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. Die logischen Grundlagen – wie sie im Stammmodul „Formale Systeme“ vermittelt werden – ähneln sich für verschiedene formale Systeme. Zum erfolgreichen praktischen Einsatz müssen die Methoden und Werkzeuge aber auf die jeweiligen Anwendungen und deren charakteristische Eigenschaften abgestimmt sein. Dies betrifft sowohl die Formalismen zur Spezifikation als auch die zur Verifikation verwendeten Techniken. Auch stellt sich bei der praktischen An­wendung die Frage nach der Skalierbarkeit, Effizienz

In der Lehrveranstaltung werden etwa fünf typische Spezifikations- und Verifikationsmethoden und -werkzeuge und die für sie jeweils typischen Anwendungsszena­rien 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 Program­me (KeY-System),
• Nachweis temporallogische Eigenschaften endlicher Strukturen (Model Checker SPIN),
• deduktive Verifikation nebenläufiger Programme (Rely-Guarantee, Isabelle/HOL),
• Systemmodellierung durch Verfeinerung (Event-B mit Rodin),
• Verifikation Hybrider Systeme (HieroMate),
• Verifikation von Echtzeiteigenschaften (UPPAAL),
• Verifikation der Eigenschaften von Datenstrukturen (TVLA),
• Programm-/Protokollverifikation durch Rewriting (Maude),
• Spezifikation und Verifikation von Sicherheitseigenschaften (KeY, JIF).

Siehe Teilleistung.

Der Gesamtarbeitsaufwand für dieses Modul beträgt 150 Stunden.

Der Aufwand setzt sich zusammen aus:

22,5h = 15 * 1,5 -  Vorlesung (Präsenz)
12h    =   8 * 1,5h - Übungen (Präsenz)
35h    Vor- und Nachbereitung der Vorlesung
12h  Installation der verwendeten formalen Systeme und Einarbeitung
30h  Lösen von praktischen Aufgaben
38,5h  Vorbereitung auf die Prüfung