Modelle und Spezifikation Verteilter Systeme
Vorlesung im Wintersemester 2001/02

Abstract:

Durch die universelle Verbreitung des Internets und verteilter, interaktiver Systeme ist der Entwurf interaktiver, nebenläufiger Systeme nicht länger eine Spezialdisziplin für wenige Experten, sondern eine der Kernaufgaben jeden Informatikers. Die steigende Komplexität derartiger Programme stellt auch neue Herausforderungen an formale Methoden des Softwareenfurfs da.

Auf der Programmierebene ist eine der Hauptmethoden, die Komplexität dieser Systeme in den Griff zu bekommen, die komponentenbasierte Softwareenwicklung. Die entsprechenden kompositionellen Methoden auf formaler Ebene sind der Themenbereich dreier in diesem Jahr erschienenen Bücher: [1], [3] und [2].

In dieser Vorlesung werden wir anhand dieser Bücher zunächst kurz klassische nebenläufige Programme mit gemeinsamen Speicher und verteilte Nebenläufigkeit behandeln. Im Hauptteil der Vorlesung gehen wir auf die komponentenbasierte Softwareentwicklung, ihre Semantik, ihre Spezifikation und ihre Beweismethoden ein.

Insbesondere werden folgende Themen behandelt:

• Einführung in verteilte Programmierung
• semantische Modelle für Nebenläufigkeit (zustandsbasierte Transitionssysteme, Spurensemantik ...)
• Kompositionalität und ``Programming-in-the-large''
• semantische Modelle für Komponenten
• Spezifikation und Verifikation von Komponenten
• Real-time Aspekte

1   Unterlagen

2   Links

References

[1]

M. Broy and K. Stølen, editors. Specification and Development of Interactive Systems. Springer-Verlag, 2001.

[2]

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. to appear.

[3]

J. Misra. A Discipline of Multiprorgamming. Springer-Verlag, 2001.

This document was translated from L^AT_EX by H^EV^EA.