Verifikation nebenläufiger Programme

Vorlesung (4h) mit Übung (2h) im Wintersemester 2002/03

Basis: Vordiplom
Zielgruppe: Studierende im Hauptstudium

Vorlesung

Verifikation nebenläufiger Programme (4-stündig, Willem-Paul de Roever)
Ort:
Termin:

Übung

Übungen zu "Verifikation nebenläufiger Programme" (2-stündig)
Ort:
Termin:

Organisatorisches

Die Vorlesung am Mittwoch den 15.6 entfaellt.

Downloads

Skript zur Einfuehrung

diverse Folien

Übungsaufgaben

Inhalt

Es ist mittlerweile klar, daß die meisten Spezifikations- und Verifikationsmethoden die Grenzen ihrer Anwendbarkeit erreicht haben. Algorithmische Methoden 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 interne Details der Komponenten zu verwenden. Die zwei Hauptfragen für kompositionelle Verifikationsmethoden sind also:

Wie zerlegt man eine globale Spezifikation in Teilspezifikationen der Komponenten?
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.

Bei Fragen zur Vorlesung: {wpr|hf}@informatik.uni-kiel.de.

References

Willem-Paul de Roever, Frank de Boer, Ulrich Hannemann, Jozef Hooman, Yassine Lakhnech, Mannes Poel, Job Zwiers.
Concurrency Verification: Introduction to Compositional and Noncompositional Methods.
Published by Cambridge University Press.

Ben Lukoschus (bls@informatik.uni-kiel.de)