Beitrag zum 3. Fachgespr"ach der GI/ITG-Fachgruppe 'Formale Beschreibungstechniken f"ur verteilte Systeme', M"unchen, Juni 1993 Strukturierte Protokollverifikation in TLA Peter Herrmann, Heiko Krumm Universit"at Dortmund, FB Informatik, LS IV Kurzfassung Zur rechnergest"utzten Analyse und Verifikation von Kommunikationsprotokollen und verteilten Systemen stehen verschiedene Techniken zur Verf"ugung. Bei Systemen mit unbeschr"anktem oder sehr gro"sem Zustandsraum bleibt (wenn man nicht endliche Vereinfachungen analysieren will) nur der Weg der logischen Verifikation, der durch mechanische Pr"adikatenlogik-Theorembeweiser und/oder Termersetzungsbeweiser unterst"uzt werden kann. In der Praxis erweisen sich logische Verifikationen jedoch auch bei Einsatz eines leistungsf"ahigen Theorembeweisers als sehr personalaufwendig. Die Beweise m"ussen sorgf"altig geplant und durch kreative Strukturierung vorbereitet werden. Der Nutzer mu"s dem System geeignete Invarianten, Axiomensysteme der verwendeten Datentypen, Hilfss"atze und Informationen zur Beweisstrategie zur Verf"ugung stellen. Als problematisch sehen wir dabei vor allem an, da"s diese Nutzerf"uhrung des Beweiswerkzeugs in Termen des Beweiswerkzeugs und nicht in problembezogenen Konzepten erfolgt. Unser Ansatz ist auf die problembezogene Strukturierung der Verifikation ausgerichtet. Er basiert auf der Spezifikation des Protokolls und des zu erbringenden Dienstes jeweils per logisch konjunktiv verkn"upfter Constraints in der Art des f"ur LOTOS-Spezifikationen von C. Vissers vorgeschlagenen Constraint-orientierten Stils. So kann z.B. eine Dienstspezifikation in die Constraints 'verlustfreie "Ubertragung in Richtung XY', 'verf"alschungsfreie "Ubertragung', 'reihenfolgetreue "Ubertragung', 'korrekte Phasenabfolge' etc., und eine Protokollspezifikation in einzelnen Mechanismen zugeordnete Constraints (z.B. 'Sequenzzahlen in Richtung XY mit Empfangspuffer und Umordnung', 'Quittierung', etc.) gegliedert werden. Die Verifikation kann dieser Strukturierung folgen. Sie kann in die Verifikationen der einzelnen Zieldienst-Constraints separiert werden. F"ur die Verifikation eines einzelnen Zieldienst-Constraints werden dabei in der Regel nur wenige der Protokoll-Constraints ben"otigt. Die Teilbeweise sowie die Protokoll-Constraints der Teilbeweise sind zwar vom Nutzer auszuw"ahlen, jedoch in problembezogenen Begriffen. Durch die Auswahl sinkt die Komplexit"at der vom Beweiswerkzeug zu erbringenden Beweise, direkt den Beweiser steuernde Eingriffe des Nutzers werden wesentlich verringert. Dar"uberhinaus kann f"ur verschiedene Protokolltypen eine Bibliothek zur Verf"ugung gestellt werden, die neben Dienst- und Protokoll-Constraint- Mustern dem Nutzer auch Beweisinformationen (Invarianten, Axiomensysteme der Kontrolldatentypen) zur Verf"ugung stellt. Die Arbeiten basieren auf der Verwendung von TLA als FDT. 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. Als Theorembeweiser wird das von W. McCune vorgestellte Werkzeug OTTER verwendet. Sein Einsatz wird durch das selbstentwickelte TLA-nach- Pr"adikatenlogik-Reduktionswerkzeug TOAST unterst"utzt. Konzeptionell werden f"ur die Fallgruppe der Transferprotokolle Dienst- und Protokoll-Constraint-Typen sowie geeignete Kombinationen und Beweisvorgaben (haupts"achlich Invarianten) erarbeitet. Der Vortrag soll Ansatz und Ergebnisse vorstellen und an einfacheren Beispielen verdeutlichen.