Modulcode:	MS1002
Englische Bezeichnung:
Modulverantwortliche(r):	Prof. Dr. Willem-Paul de Roever
Turnus:	unregelmäßig (SS07)
Präsenzzeiten:	4V 2Ü
ECTS:	8
Workload:	240 Std.
Dauer:	ein Semester
Modulkategorien:	TG (Sonstige) MV (Sonstige)
Lehrsprache:	Deutsch
Voraussetzungen:

Kurzfassung:

Die meisten Spezifikations- und Verifikationsmethoden haben die Grenzen ihrer Anwendbarkeit erreicht. Algorithmische Methoden (z.B., Modelchecking) können endliche Systeme nur bis zu einer bestimmten Größe überprüfen, während deduktive Methoden nur für Systeme geringer Komplexität geeignet sind, weil sie von intensiver Benutzerinteraktion abhängig sind. Die einzige Hoffnung, formale Verifikation für Probleme von industrieller Größe einzusetzen, baut auf die Anwendung zweier wichtiger Prinzipien: Kompositionalität und Abstraktion. Kompositionelle Verifikationsmethoden ermöglichen es, Eigenschaften eines zusammengesetzten Systems aus den Spezifikationen seiner Teile herzuleiten, ohne die Implementierung dieser Teile zu verwenden. Nach der Behandlung der Grundlagen traditioneller, nicht-kompositioneller Beweismethoden liegt der Schwerpunkt auf der Entwicklung kompositioneller Beweismethoden für nebenläufige Programme.

Lernziele:

In diesem Modul erlernern die Studierenden die Techniken der kompositionellen Verifikation.

Lehrinhalte:

Kompositionelle Verifikationsmethoden ermöglichen es, Eigenschaften eines zusammengesetzten Systems aus den Spezifikationen seiner Teile herzuleiten, ohne interne Details der Komponenten zu verwenden. Die zwei Hauptfragen für kompositionelle Verifikationsmethoden sind also:

1. Wie zerlegt man eine globale Spezifikation in Teilspezifikationen der Komponenten?
2. Wie schließt man aus der Erfülltheit der Teilspezifikationen auf die Erfülltheit der globalen Spezifikation?

Nach der Behandlung der Grundlagen traditioneller, nicht-kompositioneller Beweismethoden liegt der Schwerpunkt der Vorlesung auf der Entwicklung kompositioneller Beweismethoden für nebenläufige Programme.

Weitere Voraussetzungen:

Prüfungsleistung:

Mündliche Prüfung am Vorlesungsende

Lehr- und Lernmethoden:

Verwendbarkeit:

Literatur:

W.-P. de Roever et al.:Concurrency Verifikation: Introduction to Compositional and Noncompositional Proof Methods. Cambridge Univ. Press, 2001.

Gregory R. Andrews, Foundations of Multithreaded, Parallel, and Distributed Programming. Addison Wesley, 2000.

Verweise:

Kommentar: