Informatik-Fachberichte 247 Herausgeber: W Brauer im Auftrag der Gesellschaft fOr Informatik (GI) Springer-Verlag Geschaftsbibliothek - Heidelberg Heiko Krumm Funktionelle Analyse von Kommunikations protokollen Springer-Verlag Berlin Heidelberg New York London Paris Tokyo Hong Kong Barcelona Autor Heiko Krumm Universitat Dortmund, Fachbereich Informatik, LS IV Postfach 500500, 0-4600 Dortmund 50 CR Subject Classification (1987): C.2, F.3.1, 0.1.3 ISBN-13:978-3-540-52854-8 e-ISBN-13:978-3-842-84246-7 001: 10.1007/978-3-842-84246-7 Dieses Werk ist urheberrechtlich geschOtzt. Die dadurch begrOndeten Rechte. insbesondere die der Obersetzung, des Nachdrucks, des Vortrags. der Entnahme von Abbildungen und Ta bellen. der Funksendung, der Mikroverfilmung oder der VervielfAltigung auf anderen Wegen und der Speicherung in Datenverarbeitungsanlagen. bleiben. bei auch nur auszugsweiser Verwer tung, vorbehalten. Eine VervielfAltigung dieses Werkes oder von Teilen dieses Werkes ist auch im Einzelfall nur in den Grenzen der gesetzlichen Bestimmungen des Urheberrechtsgesetzes der Bundesrepublik Deutschland yom 9. September 1965 in der Fassung Yom 24. Juni 1985 zulAssig. Sie ist grundsAtzlich vergOtungspflichtig. Zuwiderhandlungen unterliegen den Straf bestimmungen des Urheberrechtsgesetzes. © Springer-Verlag Berlin Heidelberg 1990 2145/3140-543210 -Gedruckt auf sAurefreiem Papier Vorwort 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. Danken mOchte ich den zahlreichen Studenten, deren Studien- und Diplomarbeiten zur prototy pischen Entwicklung von Werkzeugen und zur praktischen Methodenerprobung beigetragen haben, und eben so meinen ehemaligen Kollegen am Institut fUr Telematik fUr die fruchtbare Zusammenarbeit. Die Arbeit ware in dieser Form nicht moglich gewesen ohne den Erfahrungsaustausch mit Mit arbeitern von Forschungs-und Entwicklungsabteilungen der Informatik- und Telekommunika tionsindustrie. Insbesondere in der Abteilung flir Grundlagenentwicklung der Firma PKI und im Europiiischen Netzwerkzentrum der Firma IBM habe ich hierzu wichtige Partner gefunden. Dem Leiter des Instituts flir Telematik, Herro Prof. Dr. Gerhard Kruger, bin ich flir die wis senschaftliche Forderung, die giinstigen Arbeitsbedingungen und seine wertvollen Anregungen zur Ausarbeitung des Themas dankbar. Herr Prof. Dr. Peter Deussen hat mir tiber seine Funk tion als zweiter Gutachter der Habilitationsschrift hinausgehend mit seinem groBen Interesse und seiner konstruktiven Kritik sehr geholfen und zur klaren Darstellung der Grundlagen bei getragen. Auf die behandelte Problematik aufmerksam gernacht hat mich Herr Prof. Dr. Oswald Drobnik; der Erfahrungsaustausch mit ihm und seine Standpunkte zur Entwicklungspraxis von Telematik-Systemen haben meine Arbeiten wesentlich beeinfluBt. SchlieBlich mOchte ich auch meiner Farnille flir ihre Geduld und Unterstiitzung danken. Dortmund, im Miirz 1990 HeikoKrumm Inhalt 1. Einleitung 2. Systeme kommunizierender Instanzen ................................. 5 2.1 Reale Systeme ........... ... ... ... ........ ...... .......... ...... ...... ....... 6 2.2 Systemstruktur .............................................................. . 7 2.2.1 Grundstruktur ..................................................... . 8 2.2.2 Ablauforientierte Sieht 8 2.2.3 Systemfonnen 9 2.3 Instanz 10 2.3.1 Kommunikationsereignisse 10 2.3.2 Kommunikationsverhalten 11 2.3.3 Verhaltensgleiehheit .. ... ..... ....... ..... ...... ...... ...... ..... 15 2.3.4 Spraehe ............................................................ 17 2.3.5 Akzeptor .... ... .... ... ... ... ........... ...... .... ...... ......... .... 19 2.4 Kopplung ..................................................................... 20 2.4.1 Dbereinkunft-Prinzip 22 2.4.2 Ubertragung-Prinzip 24 2.5 Systemablauf .................................................................. 27 2.5.1 Gesehlossenes System . ... .... ........ ... ...... ...... ....... ....... 27 2.5.2 Offenes System ...................................................... 27 2.5.3 Systemzustand .. ... ... ... ........ ....... ...... ...... ..... ........... 28 2.5.4 Erreiehbarkeitsgraph ................................................ 31 2.5.5 Ersatzinstanz 34 3. Dienste und Protokolle 36 3. 1 Protokolle 36 3.2 Dienste 38 3.3 Kommunikationsdienste 40 3.4 Kommunikationsprotokolle 43 4. Analysemafinahmen 45 4.1 System-Priifung 46 4.1. 1 Vergleieh 46 4.1.2 Allgemeine Kriterien 47 - vrn - 4.1.2.1 Beschriinktheit und Sicherheit 47 4.1.2.2 Lebendigkeit 48 4.1.2.3 Fairness 49 4.1.2.4 Relevanz von SpezifIkationsaussagen ............... 49 4.1. 3 Spezifische Kriterien . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 4.1.4 Inspektion ......................................................... 52 4.1.4.1 Inspektionsziele .......................................... 52 4.1.4.2 Projektionen des Erreichbarkeitsgraphen .. ..... ..... 53 4.2 Protokoll-Priifung ............................................................ 54 4.2.1 Abstraktion ......................................................... 54 4.2.1.1 Protokollinstanzen und Dienstzugangspunkte 55 4.2.1.2 Rollen ...................................................... 55 4.2.1.3 Phasenstruktur 55 4.2.1.4 Kontrollparameter 56 4.2.1.5 Instanzeninterne Ablaufsteuerung .................... . 56 4.2.1.6 Nutzdaten ............................................... . 57 4.2.1. 7 Direkte Kopplung 57 4.2. 1.8 ZeittiberwachungsmaBnahmen ....................... . 58 4.2.2 MaBnahmen ........................................................ . 58 4.2.2.1 Diensttiberpriifung ...................................... . 59 4.2.2.2 Protokolltiberpriifung ................................... . 59 4.2.2.3 ProtokollverifIkation 60 4.2.2.4 Dienstableitung 60 5. Spezifikationstechniken 61 5. 1 Ubersicht und KlassifIkation 61 5.1. 1 Modellierungskonzept 61 5.1.2 Spezifikationsform 62 5.1.3 Logische Techniken 64 5.1.4 Assertionstechniken 65 5.2 Petri-Netze .................................................................... . 66 5.2.1 Modell .............................................................. . 66 5.2.2 Speziftkation ........................................................ . 69 5.2.3 Analyse .............................................................. . 72 5.3 Algebraische Speziftkationen 73 5.3.1 CCS-Grundmodell 73 5.3.2 Speziftkation ...................................................... 77 5.3.3 Analyse ............................................................... 78 - IX - 5.3.4 Nachrichtenaustausch 80 5.3.5 Varianten 81 5.4 Erweiterte endliche Automaten 82 5.4.1 Modell 83 5.4.2 Speziftkation ...................................................... 85 5.4.3 Analyse ............................................................ 87 5.4.4 Erweiterungen .................... .................................. 89 6. Strukturierter Erreichbarkeitsgraph ................ ...... .............. 91 6.1 Grundkonzept ............................................................... 91 6.2 Beispiel ........................................................................ 95 6.3 Auswertung ........... ..................... .................................. 99 6.4 Nebenlliufigkeitsmuster ................... ............. ...................... 101 7. Umgebungsmodelle ............................................................ 104 7. 1 Beispiel .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. .. . .. . .. .. . . .. .. . .. .. .. .. .. .. . .. .. .. .. .. 105 7.2 Umgebungsbewgene reduzierte Ersatzinstanz . .... ......... ........ ..... 107 7.3 Umgebungsvertrliglichkeit . . ... .. ... ... ... ... .... ... .. . ... .. . .. .... .. . ... . 110 8. Zusammenfassung 112 Literatur 113 Liste der Begriffe 119 Liste der Definitionen 121 Liste der Abbildungen 122 1 . Einleitung Die Infonnatik befaBt sich in Zukunft in verstarktem MaBe mit Systemen, die aus miteinander und mit einer Systemumgebung kommunizierenden Instanzen bestehen [26,34,46,48,70,113]. Eine Instanz flihrt nach einer ihr eigenen Vorschrift weitgehend selbstlindig und zu den tibrigen Instanzen zeitlich parallel Aktionen aus. Jede Instanz bearbeitet eine ihr zugeordnete Teilaufgabe so, daB sie zur Erftil lung eines gemeinsamen tibergeordneten Systemzwecks beitragt. Deshalb verfahren die Instanzen nicht in volliger gegenseitiger Unabhangigkeit sondern sehen auch Aktionen zur Kommunikation mit anderen Instanzen oder der Systemumgebung vor. Eine Kommunikationsaktion tragt dabei im allge meinen sowohl zur zeitlichen Abstimmung des Verhaltens einer Instanz als auch zu einem Infonna tionsgewinn flir die Instanz beL Eine Instanz kann Aktionen bis zur erfolgreichen Ausflihrung einer Kommunikationsaktion verzogern, und sie kann bei ihr anstehende Entscheidungen tiber ihr zuktinf tiges Verhalten in Abhangigkeit zum Ausgang einer Kommunikationsaktion Hillen. Dieses Systemkonzept trifft sowohl von der logischen Problemstellung her als auch im Hinblick auf die gewahlte Fonn der Losung in vielen wichtigen Anwendungsbereichen zu. So sind insbesondere Telekommunikationssysteme und Rechnernetze und darauf basierende Anwendungen wie z.B. um fassende Btiroautomatisierungs-, Produktionsplanungs- und Steuerungssysteme zu nennen [43,111, 109,106]. Hier finden sich in der Systemumgebung bereits auf Problemebene weitgehend unabhan gig und zueinander zeitlich parallel agierende Personen und technische Systeme, wahrend auch die Architektur der ProblemlOsung aufgrund der damit erzielbaren Flexibilitat, Leistungsfahigkeit und Ortsunabhangigkeit durch das Konzept kommunizierender Instanzen gepragt wird. Beim Entwurf von Systemen aus kommunizierenden Instanzen stellt sich nun allerdings im Vergleich zum Entwurf einer zentralen nur eine einzige Instanz umfassenden LOsung zusatzlich die Aufgabe, die durch die Nebenlaufigkeit mehrerer Instanzen in einer Vielzahl von Variationen moglichen AbIaufe des Gesamtsystems zu erfassen und zu verstehen. Entscheidungen zum Entwurf einer Instanz mtissen an den resultierenden Auswirkungen auf das Gesamtsystem gemessen werden. Zur Erorterung der Korrektheit des Systementwurfs muB auf alle insgesamt erreichbaren Systemzustande eingegangen werden. Ihre Anzahl ist sehr groB, da die Zustande der einzelnen Instanzen durch den voneinander doch weitgehend unabhangigen Fortschritt der Instanzen in einer Vielzahl von Kombinationen auftre ten konnen. An die Stelle der bei einer zentralen, sequentiell arbeitenden Instanz bestehenden einfa chen Folge von Aktionen tritt nun eine Mehrzahl sich in den unterschiedlichsten Systemzustanden verzweigender und vereinigender Wirkungsketten. Gleichzeitig mit dieser zusatzlichen Komplexitat tritt erschwerend auf, daB aus simultan arbeitenden und in der Regel ortlich verteilten Instanzen gebildete Systeme nur unter erschwerten Umstanden und mit zusatzlichen Kosten getestet werden konnen. AI1ein schon die Bestimmung des aktuellen globalen Systemzustands im Verlauf eines Tests ist - wenn tiberhaupt - nur mit groBem Aufwand moglich. Deshalb ist man in besonderem MaB auf Methoden angewiesen, die zur Qualitatssicherung bereits in der Entwurfsphase eingesetzt werden konnen und kostspielige Fehlentwicklungen frUhzeitig vennei den helfen. Einen Weg hierzu weisen Beschreibungsverfahren zur fonnalen Spezifikation von Instanzen und Sy stemen. Entwurfsergebnisse konnen hierrnit in kompakter und praziser Weise beschrieben werden. Zusatzlich eroffnen fonnale Spezifikationen die Moglichkeit zur im Ergebnis verlaBlichen formalen Analyse von Entwtirfen [26,103]. Ein solcher Verbund aus einer fonnalen Spezifikationstechnik und - 2 - vertragliehen Analyseverfahren bildet aueh den Kern weitergehender Methoden, die z.B. zur Kor rektheitssieherung formalismus-reglementierte Prozesse fUr den Entwurf und die Entwurfsumsetzung vorsehen konnen [39,91]. Die zu besehreibenden und untersuehenden Eigensehaften eines Systems beziehen sieh auf mogliehe Ablaufe entspreehender realer Systeme. Hier interessiert in der Regel ein Eigensehaftsspektrum, das folgende Teilaspekte iiberdeckt: - Leistungseigensehaften, - Eehtzeiteigensehaften, - Funktionalitat. Leistungseigensehaften betreffen die ffir die DurehfUhrung von Systemfunktionen benotigten Zeit dauern, die Menge umgesetzter Daten und die benotigten Ressoureen. Eehtzeiteigensehaften beziehen sieh speziell auf absolute Zeitpunkte von Aktionen und deren gegenseitige Abhangigkeiten. Unter Funktionaliilit werden die Eigensehaften zusammengefaBt, die bei Abstraktion von Realzeit- und Lei stungsaspekten noch siehtbar bleiben. Sie beziehen sieh auf die im einzelnen logiseh unterseheidbaren Typen von Aktionen und die darnit verbundenen Daten sowie auf die gegenseitige relative zeitliehe Lage von Aktionen. 1m allgemeinen sind innerhalb desselben Projekts Eigensehaften aller drei Typen zu berUeksiehtigen. Zu ihrer formalen Behandlung werden aber in der Regel sehr untersehiedliehe Modellierungskonzepte herangezogen. So basiert die Behandlung von Leistungseigensehaften meistens auf der Modell-Vor stellung eines stochastisehen Systems, bei dem -aus Aufwandsgriinden -die Details funktioneller Ei gensehaften weitgehend verdeekt werden miissen [6,118]. Umgekehrt verlangt die funktionelle Be handlung naeh einem Modell, in dem alle wesentliehen EinfluBfaktoren auf das grundlegende Verhal ten der Instanzen siehtbar bleiben. Zur Behandlung von Eehtzeiteigensehaften wird -allerdings nur fUr die als zeitkritisch eraehteten Systemteile -das funktionelle Modell erweitert [78,95]. Ansatze zur Integration versehiedener Aspekte sind in Diskussion [14,61,96,99,100]. Die vorliegende Abhandlung konzentriert sieh auf Methoden zur Behandlung der grundlegenden funktionellen Aspekte von Systemen kommunizierender Instanzen. Aueh in diesem Bereieh wird ein Sehwerpunkt gesetzt, formale Beschreibungsverfahren sowie darauf basierende Analyseverfahren. 1m Bliekpunkt liegen die im Kern aller weitergehenden Methoden stehende formale Darstellung von Ergebnissen des Systementwurfs und deren Priifung zum Zweek der friihzeitigen Entdeekung von Entwurfsfehlern. Hierbei soIl die Umsetzbarkeit der Teehniken in die Praxis beriieksiehtigt werden. Es sollen vornehmlieh so1che Teehniken im Zentrum des Interesses liegen, die hierfiir naeh heutiger Sieht gut geeignet sind. Dies hlingt nieht nur von der benotigten Vorbildung zum Umgang mit einer Teehnik und der Vertrligliehkeit der formalen Sieht mit der praktisehen System-Sieht eines Entwerfers ab sondern aueh davon, ob, in we1chem Umfang und mit we1chem Automatisierungsgrad Werkzeuge zur Unterstiitzung der Anwendung zur Verfiigung stehen, urn den Personalaufwand der Anwendung zu reduzieren und eine hohe VerlliBliehkeit ffir die Ergebnisse zu garantieren. Die Anwendung solI anhand der in ihren Anforderungen an Teehniken und Werkzeuge besonders an spruehsvollen Klasse der Telekommunikationssysteme behandelt werden. Unter Abstraktion von nur ortlich relevanten Aktionen und Konzentration auf ortsiibergreifende Interaktionen entsprieht ein Te lekommunikationssystem einem Kommunikationsprotokoll, das somit als spezielles abstraktes Sy stem kommunizierender Instanzen definiert werden kann [43, 111,120]. Hohe Qualitatsanforderungen an die verwendeten Kommunikationsprotokolle, ihre waehsende Kom plexitat sowie die hier bestehenden Normungsbestrebungen fOrdern in zunehmendem MaBe den Ein satz formaler Teehniken [30,80,102]. Sie haben bereits in den industriellen Entwieklungslabors zu einer gestiegenen Akzeptanz und verstarkten Anstrengungen zur Entwieklung besonderer Teehniken und Werkzeuge geftihrt [8,9,12,103,105,110,112]. Hierbei werden vornehmlieh konstruktive, un- - 3 - mittelbar auf der Defmition von operationalen Systemmodellen basierende Techniken eingesetzt. Sie folgen im wesentlichen drei unterschiedlichen Grundkonzepten. Zum bisher am weitesten verbreiteten Konzept gekoppelter endlicher Automaten und zu Petri-Netz-Modellen treten in den letzten Jahren al gebraische Speziflkationsmethoden. Unter einem operationalen Systemmodell sei ein Modell verstanden, in dem der reale zeitliche Ablauf eines Systems in seiner Zusammensetzung aus einzelnen Operationen noch eine direkte Entsprechung flndet. Operationale Systemmodelle bilden die wesentliche Grundlage konstruktiver Speziflkations techniken und bestimmen in ihren Eigenschaften direkt die in den Speziflkationen vorkommenden Konstrukte mit deren konzeptuellem Hintergrund. Auch bei allen iibrigen Speziflkationstechniken muG ein operationales Systemmodell angesprochen werden, urn den Bezug zwischen Formalismus und realen Systemen zu defmieren und eine Deutung von Analyseergebnissen mit ihren Implikationen auf die Architektur realer Systeme zu ermoglichen. Operationale Systemmodelle treten auch im Zusammenhang mit den gebrauchlichen Speziflkations techniken in unterschiedlichsten Auspragungen auf. Es sind eine Vielfalt an Teilkonzepten und sich teilweise iiberdeckender, teilweise zueinander jedoch unvertraglicher Begriffssysteme zu verzeichnen. Dies erschwert den gegenseitigen Vergleich und die Identillzierung grundlegender Verfahrensweisen. Nicht zuletzt erschwert es die Orientierung und mindert generell die Akzeptanz fUr den Einsatz forma ler Methoden bei den - schwerpunktmliBig mit dem Entwurf eines realen Systems befaGten -Ent wicklem. Bei groBeren, aus voneinander unabhlingig entwickelten Teilen bestehenden Systemen muG femer davon ausgegangen werden, daB auch im selben Gesamtprojekt unterschiedliche Methoden eingesetzt werden, so daB ein gemeinsames Begriffssystem und eine gegenseitige Abbildbarkeit der eingesetzten Modelle notwendig sind. 1m Hinblick auf die unterschiedlichen Auspragungen operationaler Systemmodelle wurde deshalb eine integrierende Betrachtungsweise verfolgt. Unter Wiirdigung der besonderen Beitrage einzelner Techniken sollte der Schwerpunkt auf der Herausarbeitung der Gemeinsarnkeiten liegen. Mit diesem Ziel konnte ein grundlegendes Rahmenkonzept zur operationalen Modellierung von Systemen kom munizierender Instanzen entwickelt werden. Das Rahmenkonzept deflniert ein einheitliches Begriffs system und gestattet die systematische Klassiflkation der gebrauchlichen unterschiedlichen Auspra gungen operationaler Systemmodelle. Dariiberhinaus konnten Abbildungen angegeben werden, an hand deren Speziflkationen gebrauchlicher Techniken in die Begriffswelt des Rahmenkonzepts um gesetzt werden konnen. Ferner wurde durch das Rahmenkonzept eine allgemein ausgelegte Diskus sion von Analyseverfahren moglich. Die Behandlung der Analyseverfahren erfolgt ebenfalls unter dem Blickwinkel der praktischen Um setzbarkeit. So konzentriert sie sich aufregullire, mit beschrlinkten Ressourcen realisierbare Systeme und legt das Augenmerk auf Verfahren, die mit hohem Automatisierungsgrad rechnergestiitzt ausge fiihrt werden konnen. Derartige Verfahren basieren auf der erschopfenden Berechnung und der Aus wertung der Menge erreichbarer globaler Systemzustlinde und ihrer Ubergange, der sogenannten Er reichbarkeitsanalyse [24,101,115,116,119]. Zumindest die Berechnung der Systernzustande und Uberglinge, des sogenannten Erreichbarkeitsgraphen, kann in einfacher Weise vollautomatisch aus gefiihrt werden. Problematisch fiir die Berechnung und Auswertung ist allerdings der mit der GroBe eines Systems exponentiell wachsende Speicher-und Zeitbedarf. Er kann die praktische Durchfiihr barkeit von Analysen fdr detailliert modellierte, reale Systeme in Frage stellen [53]. 1m Hinblick auf die Systemanalyse konnten -unter alleiniger Bezugnahme auf das Rahmenkonzept - zwei Vorgehensweisen zur erleichterten rechnerge-stiitzten Ausfiihrung der Erreichbarkeitsanalyse entwickelt und deflniert werden, die leicht auf die gebrauchlichen Speziflkationstechniken iibertragen werden konnen: - Zur zusammengefaBten Berechnung und Auswertung von Projektionen des Erreichbarkeitsgra phen wird ein Algorithmus vorgestellt. Er tragt zu einer wesentlichen Reduktion des Speicherbe-