Seminar: Systemmodellierung und Verifikation WS 2011/12

Inhalt

Die Modellierung kritischer Software (z.B. in Automobilen, Zugsteuerungen oder in der Flug- und Raumfahrt) mit Hilfe von Sprachen, die eine formale Semantik besitzen, erlaubt eine präzise Analyse von Eigenschaften der zugrundeliegenden Systeme. Dadurch können Fehler frühzeitig erkannt und ausgebessert werden, was zu einer Reduzierung der Kosten- und Sicherheitsrisiken eines Softwareprojekts beiträgt. Dazu werden diverse Modellierungs- und Verifikationstechniken vermehrt auch in der Industrie eingesetzt. Diese reichen von manueller Verifikation innerhalb einer Programmlogik, bis hin zur vollautomatischen Verifikation durch Model Checking oder Abstrakte Interpretation (für die Entwicklung von Hardware etwa, ist Model Checking mittlerweile ein fester Bestandteil des Entwurfszyklus). Das Seminar soll eine anwendungsorientierte Einführung geben in grundlegende Techniken aus unter anderem den folgenden Bereichen:

• Modellierungssprachen und Verifikationstechniken
• Model Checking
• Abstrakte Interpretation

Ablauf

Vorbesprechung: Mittwoch, 26. 10., Raum 3018 N, 11:30 Uhr (Anwesenheitspflicht). Die Vorbesprechung ist gleichzeitig die letzte Gelegenheit zur Anmeldung.

Das Seminar findet als Blockveranstaltung Anfang 2012 statt.

Anforderungen

• Selbständige Erarbeitung der Literatur und Einarbeitung in das jeweilige Tool.
• Schriftliche Ausarbeitung eines Berichts (ca. 12 Seiten).
• Ausarbeitung und Halten einer Präsentation (45min Vortrag und Diskussion).
• Aktive Teilnahme an den Vorträgen der anderen Teilnehmer.

Anmeldung

Per E-Mail an Gidon Ernst

Themen:

Alle Vorträge sollen Tools zur Modellierung, Programmierung oder Verifikation von Softwaresystemen vorstellen und anhand von Beispielen demonstrieren.

1. Dafny: Automatische Verifikation von objektorientierte Programmen. Basiert auf den Tools Boogie und Z3 von Microsoft.
2. Chalice: Analyse von Nebenläufigen Programmen mit Hilfe des Ownership-Konzepts. Basiert ebenfalls auf Boogie und Z3.
3. Alloy/Kodkod: Ein Tool zur vollautomatischen Suche nach Fehlern in Spezifikationen und Programmen.
4. TVLA: TVLA basiert auf Shape Analysis, einer vollautomatischen Technik zum Nachweis von Eigenschaften von Datenstrukturen im Heap, wie z.B. Bäume oder Liste. U.a. werden auch nebenläufige Programme unterstützt.
5. JStar: Ein automatisches Verifikationstool für objekt-orientierte Java-Programme, das auf Separation Logic und Abstrakter Interpretation beruht.
6. Verifast: Ein automatisches Verifikationstool für Java und C, das auf Separation Logic basiert.

Ansprechpartner

• Gidon Ernst, Tel: 0821 / 598 - 2183, Raum 3043 N

weitere Informationen zu der Lehrveranstaltung:

empfohlenes Studiensemester der Lehrveranstaltung:	Hauptstudium
Fachrichtung Lehrveranstaltung:	Master Informatik, Master Informatik & Multimedia, Diplom Informatik
Nummer der Lehrveranstaltung:	07097
Dauer der Lehrveranstaltung:	2 SWS
Typ der Lehrveranstaltung:	S - Seminar
Leistungspunkte:	4 LP
Bereich:	Softwaretechnik und Programmiersprachen (PO ab 2009), Theoretische Informatik (nur alte POs)
Prüfung:	Referat / Hausarbeit
Semester:	WS 2011/12