Entwurf verteilter Anwendungen mit TLA

Arnulf Mester, Heiko Krumm
FB Informatik, LS IV, Universit"at Dortmund


Kurzfassung

Zuk"unftigen grossen verteilten Anwendungen werden komplexe verteilte 
Algorithmen zugrundliegen, f"ur die formale Spezifikations- und 
Verifikationsverfahren erforderlich werden. Die Algorithmen werden zu 
grossen Anteilen aus Teilalgorithmen eines vorgegebenen Spektrums 
zusammengesetzt sein.
Der Beitrag befasst sich mit der Anwendung der formalen Beschreibungs-
technik TLA (L. Lamport: Temporal Logic of Actions) f"ur diesen 
Problemkreis.  Anhand eines einfach gehaltenen Beispiels werden die 
Prinzipien der Anwendung verdeutlicht und auch Ansatzpunkte zu 
methodischen Vorgehensweisen und Rechnerunterst"utzungsm"oglichkeiten 
aufgezeigt, die auf die Komposition aus Teilalgorithmen Bezug nehmen.