Inhalt
Der Begriff "reaktive Systeme" ist von Amir Pnueli geprägt worden und
beschreibt Systeme, die typischerweise eine unendliche Laufzeit haben
und dabei fortlaufend auf Stimuli ihrer Umgebung, wie etwa von anderen
Maschinen, Meßinstrumenten oder auch Menschen, reagieren. Durch ihre
unendliche Laufzeit unterscheiden sie sich von sogenannten
transformationellen Systemen, die auf eine Eingabe eine bestimmte
Ausgabe erzeugen und dann terminieren.
Reaktive Systeme bestehen oft aus mehreren Komponenten, die parallel
zueinander arbeiten und durch Nachrichtenaustausch miteinander
kommunizieren. Beispiele für reaktive Systeme finden sich im Bereich der
Steuerungs- und Kontrollsysteme (z.B. Fahrstuhlsteuerungen) oder auch bei
Telekommunikationssystemen.
In dieser Vorlesung soll einerseits eine Sprache zur
Beschreibung reaktiver Systeme (und ein semantisches Modell) und
anderseits eine Logik zur Beschreibung von Eigenschaften
vorgestellt werden. Die Sprache ist eine sogenannte Prozeßalgebra, CSP,
die Logik eine temporale Logik (PTL). Ein großer Teil der Vorlesung
wird sich mit dem Nachweis der Korrektheit von reaktiven Systemen
beschäftigen. Dies kann (teilweise) auch vollautomatisch
stattfinden. Dazu
werden zwei Werkzeuge vorgestellt werden: der Modelchecker FDR zum
Nachweis von Eigenschaften für CSP-Programme, und der Modelchecker
SPIN für
PTL. Die beiden Tools sollen praktisch ausprobiert werden
und zum Korrektheitsnachweis kleinerer verteilter Algorithmen
eingesetzt werden.
Literatur
C.A.R. Hoare: Communicating Sequential Processes, Prentice Hall,
1985.
A.W. Roscoe: The Theory and Practice of Concurrency, Prentice Hall,
1998.
Z. Manna and A. Pnueli: The temporal logic of reactive and concurrent
systems (Specification), Springer, 1991.
G.J. Holzmann: Design and Validation of Computer Protocols, Prentice
Hall, 1990.
G.J. Holzmann: The Spin Model Checker, IEEE Trans. on Software Engineering, Vol. 23, No. 5, May 1997, pp. 279-295. (gzipped postscript)