![[Technical Faculty]](../../images/tflogo.gif)
Verifikation nebenläufiger Programme
Vorlesung (4h) mit Übung (2h) im Sommersemester 2007
Basis: Vordiplom bzw. Bachelor
Zielgruppe: Studierende im Hauptstudium und Masterstudenten
Vorlesung
Verifikation nebenläufiger Programme (4-stündig,
Willem-Paul de Roever)
Ort: LMS2-R.Ü1
Termin: Montag 8:15-9:45 und Mittwoch 8:15-9:45
Übung
Übungen zu ,,Verifikation nebenläufiger Programme`` (2-stündig,
Immo Grabe)
Ort: WSP3 - R.1
Termin: Mittwoch 12:15 - 13:45
Organisatorisches
Die Übungsaufgaben werden jeweils am
Montag im Anschluß an die Vorlesung ausgegeben und Online zur
Verfügung gestellt. Die Bearbeitung der Übungsaufgaben ist
in Gruppen von zwei Personen durchzuführen. Es werden zwei
spezielle Serien von Übungsaufgaben ausgegeben, der
Mittsemestertest und der Endsemestertest. Diese speziellen Serien
sind von jedem Studenten in Einzelarbeit zu bearbeiten und abzugeben.
Sie erhalten ein höheres Gewicht bei der Notenfindung als die
normalen Übungsserien. Jede Studentin/jeder Student sollte in
der Lage sein, die abgegebenen Aufgabenlösungen in der Übung
zu präsentieren. Die Aufgabenlösungen sind in gut
leserlicher Form (als Postscript oder PDF Datei oder in sauberer
Handschrift) bis zum Montag der auf die Ausgabe folgenden Woche um
10:00 Uhr abzugeben.
Downloads
Skript zur Einfuehrung
diverse Folien
Vorlesung 20.6.
Ü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|igb}@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.
Jens Schönborn
(jes@informatik.uni-kiel.de)