In dieser Arbeit wird ein Konzept zur Beschreibung und Verifikation von Protokollen vorgestellt. Dabei wird ein Beschreibungsformalismus gewählt, der einer modallogischen Axiomatisierung durch eine Temporallogik für verzweigende Zeit zugänglich ist. Für diese Temporallogik wird ein Tableaukalkül entwickelt, mit dem die Korrektheit der Protokolle formal bewiesen werden kann.

Bei dem verwendeten Ansatz werden Protokolle durch Evolving Algebras beschrieben. Diese wurden in [Gurevich; 1988] zur Beschreibung operationaler Semantik im Sinne von Turings Satz eingeführt. Zu einem gegebenen Algorithmus können auf beliebigen Abstraktionsebenen Evolving Algebras entworfen werden, die diesen Algorithmus modellieren. Die einzelnen Berechnungszustände werden dabei durch (statische) Algebren, d.h. prädikatenlogische Strukturen, deren einziges Prädikat die Gleichheit ist, modelliert. Eine Evolving Algebra wird durch eine statische Algebra als Anfangskonfiguration und Übergangsregeln gegeben. Dies definiert einen Zustandsübergangsgraphen, der aus logischer Sicht als verzweigende temporale Kripke-Struktur aufgefaßt wird.

Zu deren Beschreibung dient eine auf den temporalen (Aussagen)-Logiken CTL bzw. CTL^* [Ben-Ari, Manna, Pnueli; 1981], [Emerson, Halpern; 1983] aufbauende Quantorenlogik inklusive Gleichheit.

Aus der Modellierung des Protokolls als Evolving Algebra wird eine Axiomatisierung in CTL-Syntax generiert. Dies kann rein syntaktisch erfolgen. Die weiteren in den Beweis eingehenden Voraussetzungen, wie z.B. die nicht in CTL beschreibbaren Fairnessannahmen, sowie die zu beweisenden Aussagen werden in CTL^* formuliert.

Es wird eine auf prädikatenlogischen Tableaux basierende Tableausemantik für Logik verzweigender Zeit entwickelt, bei der Zustände und Pfade der Kripke-Strukturen explizit benannt werden. Sie ermöglicht es, von endlich langen Pfadabschnitten zu abstrahieren, um so Erreichbarkeitsaussagen ohne graphentheoretische Zusatzalgorithmen verarbeiten zu können. Für diese Semantik wird ein Tableaukalkül für prädikatenlogisches CTL definiert. Weiter wird eine CTL^*-Formelklasse spezifiziert, mit der Fairness- und Persistenzeigenschaften, die in CTL nicht formulierbar sind, beschrieben werden können. Diese Formelklasse kann aufgrund ihrer speziellen Semantik in den Kalkül integriert werden. Zur Behandlung der in der Spezifikation vorkommenden Datenstrukturen werden zusätzlich entsprechende Induktionsaxiome aufgenommen.

Für die komplette Logik CTL^* wird eine Erweiterung des Tableaukalküls angegeben.

Damit liegt ein Verfahren vor, mit dem sich (Korrektheits)beweise formal führen lassen. Um die praktische Relevanz des Verfahrens zu zeigen, wird die Korrektheit des Alternating-Bit-Protokolls basierend auf einer Modellierung als Evolving Algebra bewiesen.

Das Verfahren ist ohne Einschränkung auch auf beliebige Prozesse anwendbar, falls diese in Einzelschritte zerlegbar sind.

• Diploma Thesis (in german)
• Case study "Alternating-Bit-Protokoll" (in german).
• parts of the diploma thesis have been published in
  A Tableau Calculus For First-Order Branching Time Logic, Wolfgang May, Peter H. Schmitt, International Conference on Formal and Applied Practical Reasoning (FAPR'96), Bonn, Germany, 1996, Springer LNCS 1085, pp. 399-413.