Beitrag zum 3. Fachgespr"ach der GI/ITG-Fachgruppe 'Formale Beschreibungstechniken f"ur verteilte Systeme', M"unchen, Juni 1993 Animation von TLA-Spezifikationen Arnulf Mester, Heiko Krumm Universit"at Dortmund, FB Informatik, LS IV Kurzfassung Der Einsatz formaler Spezifikationstechniken bei der Entwicklung von Kommunikationssystemen und verteilten Anwendungen bringt auf der einen Seite - verglichen mit einer auf formale Spezifikationen verzichtenden Vorgehensweise - nat"urlich einen zus"atzlichen Aufwand mit sich. Er soll deshalb in verschiedenen Phasen des Entwicklungsprozesses zur Produktivit"atssteigerung und Qualit"atssicherung f"uhren und in der Regel werden dazu die Unterst"utzung von Entwurf, Test und Wartung durch klare Vorgaben und Ergebnisdarstellungen, die Unterst"utzung der Wiederverwendbarkeit durch pr"azise und kompakte Baustein-Spezifikationen, die fr"uhe Entdeckung von Entwurfsfehlern durch formale Verifikation, das rechnergest"utzte Testen sowie in neuerer Zeit auch die rechnergest"utzte Programmerzeugung genannt. Zumindest im derzeit dominierenden erstgenannten Aufgabenbereich mu"s die formale Spezifikation vom Menschen gelesen und verstanden werden. In der Praxis zeigt sich hier oft, da"s auch eine an sich eindeutige formale Spezifikation mi"sverstanden werden kann und trotz Kompaktheit und Strukturierung erheblichen Einarbeitungsaufwand verursacht. Vor allem die Einarbeitung und Schulung von Entwicklungspersonal in vorgegebene Spezifikationen (z.B. Protokollstandards, Spezifikationen firmeninterner Baustein-Sammlungen) sowie die R"uckkopplung beim 'Korrekturlesen' entworfener Spezifikationen gegen die (naturgem"a"s nicht vollst"andig formal erfa"sbare) Intention der Entwerfer k"onnen sich als problematisch erweisen. Zur Unterst"utzung in diesem Aufgabenbereich untersuchen wir derzeit zwei Ans"atze. Ein erster Ansatz "ubertr"agt die im Programmwartungssektor verfolgte Idee der Darstellung formaler Dokumente als Hypertext-Strukturen auf formale Spezifikationen verteilter Systeme und f"uhrte zu einem Browser-Werkzeug, das den Umgang mit dem Dokument w"ahrend des Lesens unterst"utzt. Der zweite Ansatz folgt der auch bekannten FDT-Compilern und FDT- Interpretern zugrundeliegenden Idee der maschinellen Ausf"uhrung formaler Spezifikationen, orientiert sich aber zus"atzlich an neueren Ergebnissen aus dem Gebiet der Algorithmenanimation. Dort werden vorrangig zu Schulungszwecken (bisher in der Regel sequentielle) Algorithmen in ihrem Ablauf anhand verschiedener (auch nutzerdefinierbarer) Sichten visualisiert (und zum Teil auch akustisch) 'erfahrbar' belebt. Der Vortrag soll die aktuellen Arbeiten des Animationsansatzes vorstellen. Als FDT verwenden wir TLA+, eine Sprache zur modularen Notation von TLA- Formeln. TLA ist dabei die 'Temporal Logic of Actions', eine Linearzeit- Temporallogik "uber Zustandspaaren, die 1990 von L. Lamport vorgeschlagen wurde und sowohl 'Estelle-artige' konstruktive Spezifikationen als auch 'formelorientierte' deskriptive erm"oglicht. Die Animation von TLA+-Spezifikationen basiert auf der Definition einer effizient ausf"uhrbaren TLA+-Untermenge und einem entsprechenden Interpretier-Werkzeug. Als Animationssystem werden die f"ur sequentielle Algorithmen von M. Brown vorgestellten System ZEUS und TR/VIDEO verwendet, die in sehr komfortabler Weise die Definition von Sichten und Instrumentierung von Algorithmendefinitionen unterst"utzt. Die Kopplung von Interpreter und Animationssystem erlaubt nun Experimente zur Erprobung verschiedener Animationskonzepte f"ur Kommunikationsprotokolle und verteilte Anwendungen. Die Animationskonzepte werden durch die Definition von Sichten-Typen und Vorschl"age zu ihrer Anwendung bei verschiedenen Algorithmen- und Unteralgorithmentypen (d.h. z.B. Protokollen und Protokollmechanismen) gepr"agt. Es kommen dabei nicht nur die von sequentiellen Algorithmen her bekannten Sichten sondern auch neue auf Verteilung, Transfer und Kommunikation eingehende zum Einsatz.