Veranstalter: Dr. Ulrich Hannemann Dr. Jan Bredereke

Auf dieser Seite werden während des Semesters weiterführende Informationen bereitgestellt.

Inhalt dieser Seite

• Termine
• Überblick
• Veranstaltungsinhalte
• Übungsaufgaben
• Leistungsnachweise
• Literatur

Termine:

Überblick

Dieser Kurs behandelt Verfahren, mit denen nachgewiesen werden kann, dass ein Programm geforderte Eigenschaften auch tatsächlich gewährleistet. So wird eine einfache mathematische Theorie der Programmverifikation entwickelt, die beweisbar korrekt und vollständig ist, die sog. "Inductive Assertions Method". Diese wird im Weiteren auf nebenläufige Programme erweitert, die über gemeinsame Variablen oder Versenden von Nachrichten miteinander kommunizieren. Nach der Behandlung der Grundlagen dieser nicht-kompositionellen Beweismethoden liegt der Schwerpunkt des Kurses auf der Entwicklung kompositioneller Beweismethoden für nebenläufige Programme. Kompositionelle Verifikationsmethoden ermöglichen es, Eigenschaften eines zusammengesetzten Systems aus den Spezifikationen seiner Teile herzuleiten, ohne interne Details der Komponenten zu verwenden.

Veranstaltungsinhalte

• Grundlagen: Sequentielle Programme
  • Sequentielle Transitionssysteme, Programme, Berechnungen: Auszüge aus [deR+01] als pdf.
  • Spezifikationen, Korrektheit von Programmen: Auszüge aus [deR+01] als pdf.
  • Beweismethode: Induktive Zusicherungen: Auszüge aus [deR+01] als pdf.
  • Korrektheit, Vollständigkeit: Auszüge aus [deR+01] als pdf.
  • Totale Korrektheit: Auszüge aus [deR+01] zum Begriff der Konvergenz und zu regulärer Terminierung.
• Nebenläufigkeit über gemeinsame Variablen
  • Nebenläufige Transitionssysteme: Auszüge aus [deR+01] als pdf.
  • Eine nicht vollständige Beweismethode: Auszüge aus [deR+01] als pdf.
  • Die Beweismethode von Owicki & Gries: Auszüge aus [deR+01] als pdf.
  • Beweise zur Korrektheit und Vollständigkeit.
  • Skizzen zu Beweisschritten für totale Korrektheit.
• Nebenläufigkeit über Kanalkommunikation:
  • Synchrone Transitionssysteme: Auszüge aus [deR+01] als pdf.
  • Beweismethoden für synchrone Transitionssysteme: Auszüge aus [deR+01] als pdf.
  • Entwicklung einer kompositionellen Semantik für synchrone Transitionssysteme: Auszüge aus [deR+01] als pdf, einschließlich des Äquivalenzbeweises.
  • Der Vollständigkeitsbeweis aus [deR+01] als pdf enthält auch Beweisdetails, die nicht in der Veranstaltung besprochen wurden.
• Kompositionelle Methoden
  • Kompositionalität und Anwendung auf Kanalkommunikation in Auszügen aus [deR+01] als pdf.
  • Der Assume - Guarantee Ansatz: Idee und Anwendung für Kanalkommunikation in Auszügen aus [deR+01] als pdf.
  • Ein Assumption-Commitment Beweissystem als pdf.
  • Der Assume-Guarantee Ansatz für Nebenläufigkeit über gemeinsame Variablen: entfällt leider (siehe Kapitel 8 in [deR+01])
• Syntaxorientierte Verifikation
  • Syntax und Semantik einer sequentiellen Programmiersprache: Auszüge aus [deR+01] als postscript Datei.
  • Ein korrektes und vollständiges Beweissystem.
• Anwendungsbeispiele
  • Zur Unterstützung beim Erstellen von Beweisen kann ein geeignetes Werkzeug helfen, z.B., der Theorembeweiser PVS .

Übungsaufgaben

• Erste Übungsserie: Abgabe bis zum 15. November 2004. Zum Vorgehen bei der zweiten Aufgabe existiert eine Beispiellösung.
• Zweite Übungsserie: Abgabe bis zum 1. Dezember 2004. Die zweite Aufgabe ist auch eine empfehlenswerte Übung zur Vorbereitung auf eine Modulprüfung.
• Dritte Übungsserie: Abgabe bis zum 15. Dezember 2004. Zur zweiten Aufgabe siehe auch das Beispiel vom 1. Dezember: Dijkstras Algorithmus
• Vierte Übungsserie: Abgabe bis zum 5. Januar 2005. Weil die Feiertage dazwischenliegen - diese Aufgaben sind nicht sooooo aufwändig......
• Fünfte Übungsserie: Abgabe bis zum 19. Januar 2005.
• Die sechste (und letzte) Übungsserie: Abgabe bis zum 7. Februar 2005.

Leistungsnachweise

• Entweder durch erfolgreiches Bearbeiten von Übungsaufgaben (alle Serien bearbeitet (in Zweier- oder Dreiergruppen), mindestens 50 Prozent der Punkte erreicht) inkl. bestandenem Fachgespräch,
• oder durch eine bestandene mündliche Prüfung (aka Modulprüfung).

Literatur

[deR+01] Willem-Paul de Roever, Frank de Boer, Ulrich Hannemann, Jozef Hooman, Yassine Lakhnech, Mannes Poel, and Job Zwiers.

Concurrency Verification: Introduction to Compositional and Noncompositional Methods xxiv+776 pages, 5 tables, 84 figures, and 156 excercises; ISBN 0 521 80608 9; £80/US$120. Cambridge Tracts in Theoretical Computer Science 54, Cambridge University Press, November 29, 2001.

[AO97] Krzysztof R. Apt, Ernst-Rüdiger Olderog

Verification of Sequential and Concurrent Programs . Springer Texts in Computer Science, 2nd ed., 1997. ISBN 0-387-94896-1.