Funktionelle Analyse von Kommunikationsprotokollen

Aufgrund des wachsenden Bedarfs an Kommunikationsprotokoll-Implementierungen zur Bil­ dung von Rechnemetzen und modemen Telekommunikationssystemen wurden im letzten Jahr­ zehnt unterschiedlichste formale Beschreibungsverfahren ftir Kommunikationsdienste und Pro­ tokolle vorgestellt, so z.B. auch die von intemationalen Normungsgremien unterstiitzten Spezi­ fikationssprachen SDL, ESTELLE und LOTOS. Sie unterstiitzen die klare und kompakte Defi­ nition von Diensten und Protokollen, wie sie im Sinne der Normung als verbindliche Imple­ mentierungsvorgaben benotigt werden. Auf der Basis derartiger Speziftkationssprachen konnen nebenliiufige und verteilte Systeme in ihrer Funktionalitiit und Struktur formal modelliert wer­ den. Damit eroffnen sich Moglichkeiten zur formalen Auswertung hinsichtlich der Synthese von Implementierungen und der Uberpriifung von Entwiirfen. Das vorliegende Buch soIl die Einflihrung formaler Speziftkationen und AnalysemaBnahmen in die Praxis fOrdem. Hier bestehen zum Teil gegenwartig noch erhebliche Ressentiments, die mit Hinweisen auf die Vielfalt der unterschiedlichen Methoden und den zur Anwendung erforderli­ chen groBen Personalaufwand begrtindet werden. Schwerpunkte des Buchs liegen deshalb auf der Erkliirung der verschiedenen Spezifikationskonzepte aus einer einheitlichen Sicht, auf der Darstellung von Moglichkeiten zur rechnergesttitzten automatisierten Durchflihrung von Analy­ semaBnahmen und auf der beispielhaften Verdeutlichung ihrer Anwendung. Zum letztgenannten Punkt wurde der Bereich der Telekommunikationsprotokolle gewiihlt. Der Inhalt des Buchs faBt Erfahrungen und Arbeitsergebnisse zusammen, die ich im Laufe meiner Tiitigkeit als wissenschaftlicher Mitarbeiter und Hochschulassistent am Institut flir Tele­ matik der Universitiit Karlsruhe bei der Entwicklung komplexer verteilter Systeme und ent­ wicklungsunterstiitzender Werkzeuge gewinnen konnte. Der Text wurde von der Fakultiit fUr Informatik der Universitiit Karlsruhe im Jull 1989 als Habilitationsschrift anerkannt.