[Technical Faculty]

Kompositionelle Verifikation nebenläufiger Programme
Seminar im Sommersemester 2003

Vorbesprechung: keine
Termin: Freitags, 9:00
Beginn: n.V.
Ort:  
Dozent: Willem-Paul de Roever und Mitarbeiter

Die vollständigen studientechnischen Daten sind über das Univis-System zu erfragen.

Bei Fragen zum Kurs, email an Martin Steffen.



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:
  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?
In dem Seminar werden in der Hauptsache ausgewählten Kapitel aus dem entstehenden Buch ``A compositional approach to concurrency and its applications'' [2] sowie die Kapitel 8 und 12 von [1]. Je nach Umfang des Stoffes werden die Kapitel an ein oder zwei Seminarteilnehmer vergeben. Mögliche Vortragsthemen sind z.B.:
Hoare-Logik für reaktive Systeme Kapitel 5 [2], 2 Vorträge
Korrektheit von verteilten Echtzeitsystemen Kapitel 7 [2], 1--2 Vorträge
Rely-Guarantee-Methode Kapitel 8 [1], 1 Vortrag
Communication-closed layers Kapitel 12 [1], 2 Vorträge
Der Theorembeweiser PVS und der Entwurf von Echtzeitsystemen Kapitel 9 [2], 1 Vortrag


Anmeldung

Am besten per email oder vorbeikommen.

Scheinkriterium

Verlangt ist die Ausarbeitung (mit Hilfestellung natürlich) und die Präsentation eines Vortrages über das gewählte Thema. Relevant sind

Vorträge

  Termin Vortragender Thema
1. 20.6 Michael Harder Communication-closed layers
2.   Tim D'Avis Verteilte Einigung
3.   Immo Grabe

Table 1: Vorträge

Links

References

[1]
W.-P. de Roever, F. de Boer, U. Hannemann, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers. Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods. Cambridge University Press, 2001.

[2]
J. Hooman, W.-P. der Roever, P. Pandya, Q. Xu, P. Zhou, and H. Schepers. A Compositional Approach to Concurrency and its Applications. to be published, 2003.
Pages last (re-)generated June 20, 2003
This document was translated from LATEX by HEVEA.