Spezifikation verteilter Systeme mit TLA(+)

Arnulf Mester
Lehrstuhl Informatik IV, Universit"at Dortmund

Vortrag zum 2. Fachgespr"ach der GI/ITG Fachgruppe 
'Formale Beschreibungstechniken f"ur verteilte Systeme', 
Magdeburg, Juni 1992

Inhaltsangabe

Vorgestellt werden sollen aktuelle Arbeiten zur rechnergest"utzten 
Spezifikation von Kommunikationsprotokollen und verteilten Systemen. 
Als Spezifikationssprache wird vorwiegend TLA+ [Lam92] verwendet. 
Die Arbeiten verfolgen das Ziel, den praktischen Umgang mit formalen 
Spezifikationen beim Systementwurf und bei der Implementierung zu 
erleichtern.  TLA+ ist eine Notation f"ur die Spezifikation 
nebenl"aufiger Systeme, die durch einfache Textsubstitution in
f"ur die Verifikation relevantes TLA [Lam91] "uberf"uhrt werden kann. 
Durch Anleihen bei der Spezifikationstechnik Z und programmiersprachartigen 
Notationen kommt TLA+ im Vergleich zum reinen TLA dem Einsatz bei 
praktischen Problemstellungen entgegen.

Neben Hilfen f"ur den Spezifizierer, n"amlich die rechnergest"utzte 
Spezifikation mittels syntaxorientierten Editoren betrachten wir auch 
Hilfen im Sinne von Richtlinien und Stilen f"ur bestimmte Problembereiche.
Die von Vissers, Scollo und van Sinderen [Vis88] vorgestellten und 
charakterisierten Spezifikationsstile (monolithic, state-oriented, 
constraint-oriented, resource-oriented) tragen hier zur Spezifikationshilfe 
f"ur TLA+ Spezifikationen bei. Die konstruktive Sicht eines Systems als 
Ansammlung von Komponenten und expliziten Schnittstellen hilft unserer 
Erfahrung nach ebenfalls. Diese Systemauffassung wurde auch in TA [Har89]
verfolgt und bei uns verallgemeinert [xTA90]. Beides sind resourcenorientierte 
Notationen, die sich als Einschr"ankung von TLA+ auffassen lassen.

Formale Spezifikationen m"ussen u.a. durch Implementierer genutzt, d.h. u.a. 
verstanden werden. In diesem Bereich wird die Animation, sowie die 
Vergr"oberung von Spezifikationen verfolgt.
F"ur die Animation existiert derzeit ein unter X-Windows laufendes 
Programmsystem zur Interpretation bzw. Ablaufvisualisierung von 
xTA-Spezifikationen. Eine "Ubertragung dieses Animators auf TLA+ ist in
Arbeit.
Eine Lesehilfe durch Vergr"oberung von Spezifikationen wurde f"ur Estelle unter
sucht [Wie91]. Es ist beabsichtigt, auf dieser Grundlage auch die 
Vergr"oberung von TLA(+)-Spezifikationen zu betrachten.
Desweiteren wird die Verwendung von Multimedia in der Animation von 
Spezifikationen gepr"uft. Dabei sollen aufbauend auf dem existierenden 
Animator die sequentielle Systeme betrachtenden Ans"atze von Brown
[Bro85,Bro91] Verwendung finden und der Visualisierungsaspekt (und dann 
nat"urlich 'Audioalisierung') st"arker betont werden.


[Bro85] M.H. Brown, R. Sedgewick; Techniques for algorithm animation; IEEE 
Software, 2(1):28-39, Januar 1985

[Bro91] M.H. Brown, J. Hershberger; Color and Sound in Algorithm Animation; 
Research Report, Digital Systems Research Center, 1991

[Wie91] F. Wiesenfeller, Rechnergest"utzte Aufbereitung von Protokoll-
spezifikationen, Diplomarbeit, Universit"at Dortmund, Fachbereich 
Informatik, 1991

[Har89] P.K. Harter; Writing formal specifications using Transition Axioms; 
Manuskript, DEC Marlboro, 1989

[Lam91] L. Lamport; The temporal logic of actions; Research Report, Digital 
Systems Research Center, 1991

[Lam92] L. Lamport; TLA+: Syntax and semantics; Research Report, Digital 
Systems Research Center, 1992

[Vis88] C.A. Vissers, G. Scollo, M. van Sinderen; Architecture and 
specification style in formal descriptions of distributed systems, 
in: S. Aggarwal, K. Sabnani (Ed.): Protocol Specification, Testing and 
verification VIII S. 189-204, 1988

[xTA90] R. Grote, P. Herrmann, H. Krumm; Modulare Spezifikationen basierend 
auf TA-Spezifikationen; Arbeitspapier, Informatik IV, Universit"at 
Dortmund, 1990