Brandenburgische Technische Universität Cottbus Lehrstuhl Rechnernetze und Kommunikationssysteme Protocol Engineering Entwurf und Validierung von Protokollen und Verteilten Systemen Wintersemester 2013/14 Prof. Dr.-Ing. Hartmut König http://www-rnks.informatik.tu-cottbus.de/ Lehre BTU Cottbus, LS Rechnernetze und Kommunikationssysteme, Lehrstuhlinhaber: Prof. Dr.-Ing. H. König 03013 Cottbus, Postfach 10 13 44,Telefon: 0355/69-2236 Fax: 0355/69-2127 II. Formale Beschreibungsmethoden und -techniken Kapitel 7 + 8 Protocol Engineering Wintersemester 2013/14 II.1/2 © Prof. Dr. H. König Struktur einer Protokollbeschreibung Zwei Bestandteile: Beschreibung der Datenformate Grundlage/Voraussetzung der Funktionsweise von Protokollen Beschreibung der Protokollablaufs Hauptteil der Beschreibung Wird zuerst betrachtet Die Begriffe Spezifikation und Beschreibung werden synonym verwendet !!! Protocol Engineering Wintersemester 2013/14 II.1/3 © Prof. Dr. H. König II.1 Formale Beschreibungsmethoden Abschnitt 7.3 Protocol Engineering Wintersemester 2013/14 II.1/4 © Prof. Dr. H. König Formale Beschreibungsmethoden Formale Beschreibungsmethoden sind Verfahren für die Beschreibung von Kommunikationsprotokollen und verteilten Systemen bzw. des Verhaltens der darin enthaltenen Instanzen. Sie bilden die Grundlage für die semantischen Modelle der formalen Beschreibungstechniken. Beispiele: Zustandsautomaten, Petri Netze, Prozessalgebren u. a. Erlauben i.d.R. keine vollständigen Beschreibungen Arten von Beschreibungsmethoden Konstruktive Methoden Deskriptive Methoden Protocol Engineering Wintersemester 2013/14 II.1/5 © Prof. Dr. H. König A) Konstruktive Methoden Protocol Engineering Wintersemester 2013/14 II.1/6 © Prof. Dr. H. König Konstruktive Methoden (1) Konstruktive Methoden beschreiben das Protokoll/System durch ein abstraktes Modell, dessen Ausführung bestimmt, wie sich das System bzw. die Protokollinstanzen verhalten sollen. Interpretationsvorschrift wird durch die Semantik der Methode bestimmt Quasi-Implementierung abstraktere Beschreibung Beispiele: - endliche Zustandsautomaten - Labeled Transition Systems Protocol Engineering Wintersemester 2013/14 II.1/7 © Prof. Dr. H. König Beispiel: Endlicher Zustandsautomat b/z a/x B A a/x τ/x C b/z d/x b/x Protocol Engineering Wintersemester 2013/14 II.1/8 © Prof. Dr. H. König Konstruktive Methoden (2) Vorteile: Beschreibung von Verhalten/Abläufen direkte Unterstützung des Entwurfs und der Implementierung unterstützt die Ausführung der Spezifikationen Rapid Prototyping Validation des Entwurfs Nachteile: keine explizite Darstellung wünschenswerter/einzuhaltener System-Eigenschaften Protocol Engineering Wintersemester 2013/14 II.1/9 © Prof. Dr. H. König B) Deskriptive Methoden Protocol Engineering Wintersemester 2013/14 II.1/10 © Prof. Dr. H. König Deskriptive Methoden (1) Deskriptive Methoden beschreiben Eigenschaften, die das Protokoll bzw. das verteilte System erfüllen muss. Unterlegen keine spezielle Interpretationsvorschrift Keine Beschreibung eines Algorithmus Beschriebene Eigenschaften: Sicherheitseigenschaften Lebendigkeitseigenschaften Beschreibung i.d.R. durch Temporale Logiken Protocol Engineering Wintersemester 2013/14 II.1/11 © Prof. Dr. H. König Sicherheitseigenschaften (Safety properties) Sicherheitseigenschaften besagen, dass in dem zu beschreibenden System/Protokoll bestimmtes unerwünschtes Verhalten nicht eintreten wird. Wenn etwas passiert, dann handelt es sich um etwas Erwünschtes. Beispiel XDT: keine dem Diensterbringer übergebene Dateneinheit geht verloren Sicherheitseigenschaften sind bereits erfüllt, wenn nichts passiert !!! Protocol Engineering Wintersemester 2013/14 II.1/12 © Prof. Dr. H. König Lebendigkeitseigenschaften (Liveness properties) Lebendigkeitseigenschaften sichern, dass die spezifizierten Ereignisse und Zustände irgendwann tatsächlich eintreten. Beschreiben, was passieren muss aber nicht als Algorithmus Beispiel XDT: Erreichen der Datentransferphase nach erfolgreichem Verbindungsaufbau Protocol Engineering Wintersemester 2013/14 II.1/13 © Prof. Dr. H. König Deskriptive Methoden (2) Vorteile: direkte Formulierung gewünschter Eigenschaften abgeleitete Eigenschaften sind verifizierbar Nachteile: i. Allg. nicht entscheidbar, ob die Spezifikation das erlaubte Verhalten vollständig beschreibt kein Prototyping möglich keine direkte Ableitung von Implementierungen kompliziert aufwendig bedarf Erfahrung Protocol Engineering Wintersemester 2013/14 II.1/14 © Prof. Dr. H. König C) Klassifikation Protocol Engineering Wintersemester 2013/14 II.1/15 © Prof. Dr. H. König Wichtige Beschreibungsmethoden Endliche Zustandsautomaten Erweiterte endliche Zustandsautomaten Petri-Netze Prozessalgebren Temporale Logiken Hybride Methoden Höhere Programmiersprachen sind keine formale Beschreibungsmethode !!! keine formale Semantik zu implementierungsnah Protocol Engineering Wintersemester 2013/14 II.1/16 © Prof. Dr. H. König Klassifikation der Beschreibungsmethoden Spezifikationsmethoden konstruktiv Klassifikatoren zustandsorientiert deskriptiv transitionsorientiert prozessorientiert Methoden FDTs ablauf-/interaktionsorientiert Endliche Zustandsautomaten Prozessalgebren Zeitablaufdiagramme Petri-Netze Petri-Netze Petri-Netze SDL Protocol Engineering Wintersemester 2013/14 SDL Lotos (cTLA) MSC II.1/17 Temporale Logiken cTLA © Prof. Dr. H. König II.2 Formale Beschreibungstechniken Abschnitt 7.1 Kapitel 8 Protocol Engineering Wintersemester 2013/14 II.1/18 © Prof. Dr. H. König Formale Beschreibungstechniken Formale Beschreibungstechniken sind Spezifikationssprachen, die für die Beschreibung von Kommunikationsprotokollen und verteilten Systemen entwickelt worden und eingesetzt werden. Formal definierte Syntax und Semantik formale Semantik soll eindeutige Interpretation der Spezifikationen sichern Beispiele: SDL, Lotos, cTLA → Betrachtung in den folgenden Abschnitten Erlauben eine (weitgehend) vollständige Beschreibung !!! Protocol Engineering Wintersemester 2013/14 II/19 © Prof. Dr. H. König Anforderungen an formalen Beschreibungstechniken An formale Beschreibungstechniken werden wie an Programmiersprachen bestimmte Anforderungen bzgl. ihrer Eignung für den Entwurf, für die Beschreibung und für ihre Eignung für die Validation des Entwurfs gestellt. Diese Anforderungen werden von den existierenden Formalen Beschreibungstechniken unterschiedlich erfüllt. Dies kann an den im Folgenden vorgestellten Techniken selbst beurteilt werden. Protocol Engineering Wintersemester 2013/14 II/20 © Prof. Dr. H. König Wichtige Anforderungen an formalen Beschreibungstechniken präzis, eindeutig, vollständig Vermeiden mehrdeutiger Interpretationen und unvollständiger Realisierungen implementierungsunabhängig Unterstützung von Realisierungen in verschiedenen Ablaufumgebungen verständlich Unterstützung eines intuitiven Verständnisses Vermeiden von Fehl-Interpretationen modular, veränderbar Unterstützung von Modifikationen und Erweiterungen der Spezifikationen Protocol Engineering Wintersemester 2013/14 II.1/21 © Prof. Dr. H. König II.3 Methoden und Techniken der formalen Beschreibung Abschnitt 7.4 Kapitel 8 Protocol Engineering Wintersemester 2013/14 II.1/22 © Prof. Dr. H. König Vorbemerkung In diesem Abschnitt werden die wichtigsten Beschreibungsmethoden und kurz ein Beispiel für eine zughörige Beschreibungstechnik für Kommunikationsprotokolle und Verteilte Systeme vorgestellt. Letztere beschränkt auf die Grundlagen der FDTs. Es ist nicht das Ziel dieser Vorlesung, die FDTs einzuführen. Jede der vorgestellten Methoden/Techniken repräsentiert eine unterschiedliche Herangehensweise an die Beschreibung . Zur Veranschaulichung und zum Vergleich der verschiedenen Herangehensweisen verwenden wir Beschreibungen des XDT-Protokolls, die unter http.//www.protocol_engineering.tu-cottbus.de/ XDT eingesehen werden können. Man beachte, dass mit jeder Beschreibungsmethode/-technik ein bestimmtes Denkmodell verbunden ist, das die Beschreibung bestimmter Systemaspekte fördert, die anderer aber wieder begrenzt !!! Protocol Engineering Wintersemester 2013/14 II.1/23 © Prof. Dr. H. König II.3.1 Automatenorientierte Beschreibung Abschnitt 7.4 + Kapitel 8 Protocol Engineering Wintersemester 2013/14 II.1/24 © Prof. Dr. H. König II.3.1.1 Endlicher Zustandsautomat Abschnitt 7.4 Protocol Engineering Wintersemester 2013/14 II.1/25 © Prof. Dr. H. König Endlicher Zustandsautomat (Finite State Machine, FSM) Ein endlicher Zustandsautomat ist ein Quintupel <S,I,O,T,s0> mit S - endliche, nicht leere Menge von Zuständen, I - endliche, nicht leere Menge von Eingaben, O - endliche, nichtleere Menge von Ausgaben, T S (I {τ}) O S - eine Zustandsüberführungsfunktion und s0 S - Initialzustand des Automaten. Eine Transition t T ist definiert durch das Quadrupel <s,i,o,s'>, wobei s S den aktuellen Zustand, i I eine Eingabe, o O die zugehörige Ausgabe und s' S den Folgezustand bezeichnen. τ I bezeichnet eine leere Eingabe spontane Transition Protocol Engineering Wintersemester 2013/14 II.1/26 © Prof. Dr. H. König Beispiel: Endlicher Zustandsautomat b/z Spontane Transition Eingabe-/Ausgabeereignis a/x A a/x τ/x B C b/z d/x Zustand Transition b/x Protocol Engineering Wintersemester 2013/14 II.1/27 © Prof. Dr. H. König Beispiel: XDT-Empfänger-Instanz FSM-Darstellung der XDT-Empfängerinstanz Animation XDT-Empfänger-Instanz Protocol Engineering Wintersemester 2013/14 II.1/28 © Prof. Dr. H. König Endliche Zustandsautomaten Vorteile: natürliche Beschreibung für das Verhalten von Protokollinstanzen Warten auf Eingaben Reaktion Ausgabe einfache Erstellung relativ geradlinige Überführung in eine Implementierung Grundlage für Testfallableitung Nachteile: keine Darstellung des Kommunikationsablaufs sehr große, wenig überschaubare Darstellungen möglich viele Zustände führen zu komplexen Automaten ■ Problem: Variable, z. B. Sequenznummern Unterteilung in Teil-Automaten Synchronisationsprobleme Reine FSM-Darstellungen werden für die Protokollbeschreibung nur begrenzt genutzt !!! Protocol Engineering Wintersemester 2013/14 II.1/29 © Prof. Dr. H. König II.3.1.2 Erweiterter endlicher Zustandsautomat Abschnitt 7.4 Protocol Engineering Wintersemester 2013/14 II.1/30 © Prof. Dr. H. König Erweiterter endlicher Zustandsautomat (1) (Extended Finite State Machine, EFSM) Ein erweiterter endlicher Zustandsautomat ist ein Tupel <S,C,I,O,T,s0,c0> mit S - endliche, nicht leere Menge von Zuständen, C = domain(v1) . . . domain(vn) - nicht leere Menge von Kontexten mit vi V, wobei V eine endliche, nicht leere Menge von Variablen und domain(vi) eine nicht leere, abzählbare Menge von Werten, der Wertebereich von vi, ist, I - endliche, nicht leere Menge von Eingaben, O - endliche, nicht leere Menge von Ausgaben, T S C (I {τ}) O S C - eine Zustandsüberführungsfunktion, s0 S - Initialzustand und c0 C - Anfangskontext des Automaten. Protocol Engineering Wintersemester 2013/14 II.1/31 © Prof. Dr. H. König Erweiterter endlicher Zustandsautomat (2) Kontext – Menge der Variablen mit ihren Wertebereichen Konkreter Kontext: Wertebelegung der Variablen Eine Transition tT ist definiert durch das Tupel <s,c,i,o,s',c'>, wobei sS den aktuellen Zustand, cC den Kontext vor Ausführung der Transition, iI eine Eingabe, oO die zugehörige Ausgabe, s'S den Folgezustand und c'C den Kontext nach Ausführung der Transition bezeichnen. τ - spontane Transition Zustände s S – Hauptzustände Zustände s S und c C - Nebenzustände Protocol Engineering Wintersemester 2013/14 II.1/32 © Prof. Dr. H. König Beispiel: XDT-Sender-Instanz Vereinfachte EFSM-Darstellung der XDT-Sender-Instanz Animation XDT-Sender-Instanz Variablen der relevanten Kontexte Await ACK: Connected: Go back N: sequ sequ, last, N, eom i, N, sequ Protocol Engineering Wintersemester 2013/14 II.1/33 © Prof. Dr. H. König Endlicher erweiterter Zustandsautomat Vorteile: natürliche Beschreibung für das Verhalten von Protokollinstanzen Warten auf Eingaben Reaktion Ausgabe einfache Erstellung weniger komplex als FSM-Darstellungen relativ geradlinige Überführung in eine Implementierung Nachteile: komplexe Automaten bei vielen Zuständen keine Darstellung des Kommunikationsablaufs weniger geeignet für Dienstspezifikationen keine direkte Testfallableitung möglich Populärste Beschreibungsmethode für Protokolle ☞ semantisches Modell der FDT SDL Protocol Engineering Wintersemester 2013/14 II.1/34 © Prof. Dr. H. König II.3.1.3 SDL (Specification and Description Language) www.sdl-forum.org Abschnitt 8.1 Protocol Engineering Wintersemester 2013/14 II.1/35 © Prof. Dr. H. König Entwicklung von SDL Beginn der Entwicklung: Mitte der 70er Jahre Ziel: Formale Beschreibung von Telekommunikationssystemen Spezifikationssprache der Telekommunikationsindustrie Entwickler: CCITT / ITU-T Study Group 10 Studienperioden: (früher) 4 Jahre SDL-88, SDL-92, SDL-96, SDL 2000, SDL 2010 Wichtige Sprachversionen: SDL-92: Einführung Objekt-Orientierung SDL-2000: Grundlegende Erweiterungen (z.B. Agentenkonzept) SDL-2010: neuste Version Protocol Engineering Wintersemester 2013/14 II.1/36 © Prof. Dr. H. König SDL-Notationen SDL/GR (Graphical Representation) graphische Notation Standard: Z.100 SDL ☞ SDL-2000: SDL wird nur noch als graphische Notation definiert !!! SDL/PR (Phrase Representation) rein textuelle Notation unterstützt Compilerentwicklung SDL/GR SDL/PR gemeinsam genutzte textuelle Sprachelemente Protocol Engineering Wintersemester 2013/14 II.1/37 © Prof. Dr. H. König A) Beschreibung der Systemstruktur Agenten Protocol Engineering Wintersemester 2013/14 II.1/38 © Prof. Dr. H. König Agenten Agenten beschreiben aktive Komponenten des zu spezifizierenden Systems. Sie sind Container für weitere Agenten, die dynmsich erzeugt werden. Ein Agent repräsentiert einen endlichen erweiterten Zustandsautomaten. Jeder Agent besitzt Arten von Agenten Blöcke Prozesse System äußerster Block Protocol Engineering Wintersemester 2013/14 eine Identifikation, eigene Lebensdauer, eine unendliche Warteschlange für Stimuli Stimuli Ereignisse, die einen Zustandsübergang (Transition) auslösen Auslöser einer Transition: jeweils das erste Ereignis in der Warteschlange II.1/39 © Prof. Dr. H. König Blöcke vs. Prozesse Blöcke und Prozesse unterscheiden sich im Ausführungsschema der enthaltenen Agenten. Blöcke können Blöcke und Prozesse enthalten nebenläufige Ausführung der EFSM des umgebenen Blockes und der enthaltenen Agenten Prozesse können nur Prozesse enthalten alternierende Ausführung der Agenten ☞ immer nur eine Transition wird ausgeführt !!! Protocol Engineering Wintersemester 2013/14 II.1/40 © Prof. Dr. H. König Beispiel für die Anordnung von SDL/GRDiagrammen block block block block block block block block system block block process process block block process Protocol Engineering Wintersemester 2013/14 II.1/41 © Prof. Dr. H. König Agenten in einer SDL-Spezifikation System Block Block Block Block Prozess Prozess Prozess Umgebung Kanal Protocol Engineering Wintersemester 2013/14 II.1/42 © Prof. Dr. H. König B) Kommunikation zwischen den Systemkomponenten Signale und Kanäle Protocol Engineering Wintersemester 2013/14 II.1/43 © Prof. Dr. H. König Kommunikation zwischen Agenten Arten der Kommunikation asynchroner Nachrichtenaustausch Signale entfernte Prozeduraufrufe Client/Server-Prinzip gemeinsame Variable read only - Zugriff auf entfernte Variable ☞ Im folgenden werden nur Signale betrachtet ! Protocol Engineering Wintersemester 2013/14 II.1/44 © Prof. Dr. H. König Signale Signale transportieren Nutzdaten im asynchronen Datenaustausch. Signale besitzen einen Namen eine implizite Senderidentifikation Deklaration in einem Textsymbol Austausch der Signale erfolgt über Kanäle Protocol Engineering Wintersemester 2013/14 II.1/45 © Prof. Dr. H. König Austausch von Signalen signal S1(Charstring, Integer,….) Textsymbol P2 P1 dcl code Charstring length Integer . . . dcl code Charstring s1(code,100,…) s1(code,length,….) Eingabesymbol Ausgabesymbol Protocol Engineering Wintersemester 2013/14 II.1/46 © Prof. Dr. H. König Kanal Ein Kanal (channel) ist ein uni- oder bidirektionaler Kommunikationspfad zwischen zwei Agenten für den Austausch von Signalen. zuverlässige, reihenfolgebewahrende Übertragung Übertragungsarten verzögernd verzögerungsfrei Gates: Endpunkte der Kanäle externe Kommunikationspunkte der Agenten implizite / explizite Gates Protocol Engineering Wintersemester 2013/14 II.1/47 © Prof. Dr. H. König Verzögernde vs. verzögerungsfreie Übertragung System Block Block Block Block Prozess Prozess Prozess Umgebung verzögernd verzögerungsfrei Protocol Engineering Wintersemester 2013/14 II.1/48 © Prof. Dr. H. König Kanäle und Gates block C verzögernder Kanal signal a,b,c,d,e,i,j,k; g1 S [a] [d] [j] c Gates [k] r1 R r3 r2 g4 [c] [b,e] Signalliste Kanal g2 Signalliste Eingabe g3 [i] Signalliste Ausgabe Protocol Engineering Wintersemester 2013/14 [i] verzögerungsfreier Kanal II.1/49 © Prof. Dr. H. König C) EFSM Beschreibung Zustände und Transitionen Protocol Engineering Wintersemester 2013/14 II.1/50 © Prof. Dr. H. König Prinzip der Beschreibung von Transitionen Ausgangszustand await_ACK Eingabe ACK sequ=1 zusätzliche Bedingung t ACK sequ≠1 reset (t) XDATconf connected Ausgabe continuousSignal internal time-out XABORTind XABORTind idle idle nextstate=await_ACK Rücksetzen Timer Folgezustand Protocol Engineering Wintersemester 2013/14 II.1/51 © Prof. Dr. H. König Eingabevarianten SDL bietet verschiedene Eingabe-Varianten an. Neben dem normalen Eingabe sind das die priorisierte Eingabe, das kontinuierliche Signal, und das save-Konstrukt. S1 a normal b prioritized Wird zuerst ausgelesen Protocol Engineering Wintersemester 2013/14 q abort continuous signal save - Stellt eine Bedingung dar - Geringere Priorität II.1/52 Siehe übernächste Folie © Prof. Dr. H. König Entnehmen von Signalen aus der Eingabewarteschlange S1 a löst Transition aus b a i a b S2 b b wird verworfen q i i j q i löst neue Transition aus Protocol Engineering Wintersemester 2013/14 II.1/53 © Prof. Dr. H. König save - Konstrukt Das Eintreffen der Ereignisse in der Warteschlange ist nicht vorhersehbar. SDL bietet deshalb die Möglichkeit, dass die Ereignisse an der Spitze der Eingabe-Warteschlange, die in diesem Zustand nicht erwartet werden, "gerettet" werden, d.h. das zweite Element wird ausgelesen, während das "gerettete" Element in der Warteschlange bleibt. k i S2 q k q i j q save Protocol Engineering Wintersemester 2013/14 II.1/54 © Prof. Dr. H. König Spontane Transition Nichtdeterministisches Verhalten kann durch spontane Transitionen, die none im Eingangs-Symbol enthalten, dargestellt werden. Die Aktivierung einer spontanen Transition hängt nicht vom Vorhandensein eines Signals in der Eingabe-Warteschlange des jeweiligen Agenten ab. break ack XDATconf connected Protocol Engineering Wintersemester 2013/14 none XABORTind idle II.1/55 © Prof. Dr. H. König D) Komposite Zustände und Zustandsaggregation Protocol Engineering Wintersemester 2013/14 II.1/56 © Prof. Dr. H. König Komposite Zustände Neben der Strukturierung von Agenten in Sub-Agenten bietet SDL-2000 auch die Möglichkeit, der hierarchischen Beschreibung von Zuständen. Kompositer Zustand: Ein Zustand, dessen Verhalten durch eine separate Zustandsmaschine beschrieben wird Bietet die Möglichkeit der Dekomposition/Untergliederung der Beschreibung hierarchische Zustandsbeschreibung alle Zustände haben eine gemeinsame Warteschlange Agent ist in mehreren Teil-Zuständen es wird immer nur eine Transition ausgeführt Protocol Engineering Wintersemester 2013/14 II/57 © Prof. Dr. H. König Komposite Zustände state S1 Prozeduren S1 state S1A c S1A exit S1A S1 a init b S2 Protocol Engineering Wintersemester 2013/14 return II.1/58 © Prof. Dr. H. König Zustandsaggregation Eine Zustandsaggregation ist eine Partitionierung eines kompositen Zustand in mehrere komposite Zustände. Die Zustandspartitionen sind statisch und können nicht adressiert werden. Die Eingabewarteschlangen der Partitionen müssen disjunkt sein. state S1 Die Transitionen der verschiedenen Partitionen werden nach dem Interleaving-Prinzip ausgeführt. state aggregation sx S1 S1 a S2 state S2 sx a S2 b b sy Protocol Engineering Wintersemester 2013/14 II.1/59 © Prof. Dr. H. König E) Ausnahmebehandlung (exception handling) Protocol Engineering Wintersemester 2013/14 II.1/60 © Prof. Dr. H. König Ausnahmebehandlung Seit SDL-2000 bietet die Sprache Konstrukte an, um Reaktionen auf unerwartetes Verhalten zu spezifizieren, z. B. bei Fehlern. Dies ist eine weitere Variante der Beschreibung interner Ereignisse. Ausnahmen werden in einem Text-Symbol spezifiziert Reaktion wird in einem Exception-Handler beschrieben, der über eine onexeption Symbol mit dem Verhalten verbunden ist Beschreibung der Reaktion beginnt mit einer handle-Anweisung Ausnahme wird explizit durch eine raise-Anweisung ausgelöst (implizite Auslösung ebenfalls definiert) Protocol Engineering Wintersemester 2013/14 II.1/61 © Prof. Dr. H. König Beispiel: Ausnahmebehandlung ExceptionDefinition exception handler on exception Zuweisung zum Verhalten exception abort connected data XDATind ACK ab ab abort data abort XABORTind idle raiseAnweisung Reaktion - Protocol Engineering Wintersemester 2013/14 handleAnweisung II.1/62 © Prof. Dr. H. König F) Objekt-Orientierung Protocol Engineering Wintersemester 2013/14 II.1/63 © Prof. Dr. H. König Objekt-Orientierung SDL ist eine objekt-orientierte Sprache, d.h. alle Agenten werden zuerst als Datentyp eingeführt. Aus historischen Gründen werden andere Begriffe verwendet als in der Objekt-Orientierung üblich. Typen ↔ Klassen Instanzen ↔ Objekte Typen u. a. Agententypen, komposite Zustandstypen, Signaltypen, einfache Datentypen Instanzen u. a. System, Block, Prozess, Signal Protocol Engineering Wintersemester 2013/14 II.1/64 © Prof. Dr. H. König G) Formale Semantik Protocol Engineering Wintersemester 2013/14 II.1/65 © Prof. Dr. H. König Formale SDL-Semantik SDL besitzt eine formale Semantik auf der Grundlage von Abstract State Machines (ASM). Statische Semantik nur für Kernsprache definiert Ableitung eines abstrakten Syntaxbaums Dynamische Semantik Ableitung eines Verhaltensmodells aus Syntaxbaum Interpretation als ASM-Kode SDL-to-ASM-Compiler Börger, E.; Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag, 2003. Protocol Engineering Wintersemester 2013/14 II.1/66 © Prof. Dr. H. König Dynamische SDL-Semantik Abstrakter Syntaxbaum Struktur Verhalten Daten Interface Compilierung Initialisierung Struktur Verbindungen Primitive Abstrakte SDL-Maschine ASM Protocol Engineering Wintersemester 2013/14 II.1/67 © Prof. Dr. H. König II.3.2 Ablauforientierte Beschreibung MSC (Message Sequence Charts) www.sdl-forum.org Abschnitt 8.2 Protocol Engineering Wintersemester 2013/14 II.1/68 © Prof. Dr. H. König Message Sequence Charts Message Sequence Charts ist eine Beschreibungssprache der ITU-T zur Darstellung/Visualisierung von Kommunikationsabläufen in Systemen. Ein Chart beschreibt einen ausgewählten Ablauf. ursprünglich nicht als FDT konzipiert Darstellung von Interaktionen zwischen Komponenten eines Systems sowie zur Umgebung Anwendungen Entwurf von Kommunikationsabläufen Dokumentationen Testfallbeschreibungen Protocol Engineering Wintersemester 2013/14 II.1/69 © Prof. Dr. H. König Entwicklung von MSC Beginn der Entwicklung: Anfang der 90er Jahre Entwickler: ITU-T Empfehlung Z.120 (MSC’92) Studienperioden: 4 Jahre MSC‘92, MSC‘96, MSC 2000 ☞ Integration in UML-2 !!! Sequenzdiagramme Protocol Engineering Wintersemester 2013/14 Wichtige Erweiterungen MSC’96 - formale Semantik (Prozessalgebren) - High-level MSC (HMSC) MSC 2000 - Datentypen - entfernte Methodenaufrufe - Objekt-Orientierung II.1/70 © Prof. Dr. H. König MSC-Notationen MSC/GR (Graphical Representation) graphische Notation ☞ praktisch relevante Notation !!! MSC/PR (Phrase Representation) rein textuelle Notation Werkzeugentwicklung MSC ist an keine bestimmte Spezifikationssprache gebunden !!! aber bevorzugt im Umfeld von SDL genutzt Protocol Engineering Wintersemester 2013/14 II.1/71 © Prof. Dr. H. König A) Message Sequence Chart Protocol Engineering Wintersemester 2013/14 II.1/72 © Prof. Dr. H. König Message Sequence Chart Ein Message Sequence Chart ist das Grundelement der Beschreibung in MSC. Es beschreibt die Interaktionen zwischen zwei oder mehreren Systemkomponenten und der Umgebung. Grundelemente: Instanzen beschreiben Systemkomponenten Nachrichten beschreiben Interaktionen Protocol Engineering Wintersemester 2013/14 II.1/73 © Prof. Dr. H. König MSC für erfolgreichen XDTVerbindungsaufbau msc XDT-Verbindungsaufbau XS XDATrequ XR DT(sequ=1) XDATind ACK XDATconf Protocol Engineering Wintersemester 2013/14 II.1/74 © Prof. Dr. H. König Zeit in einem MSC in(m1) m1 m5 m2 m4 in(m2) out(m2) m3 out(m3) in(m4) t out(m4) out(m5) Connectivity Graph Annahme einer globalen Uhr entlang einer Instanzenachse schreitet die Zeit voran (ohne Zeiteinheit) zeitliche Ordnung der Ereignisse entlang der Instanzenachse Senden und Empfangen von Nachrichten sind asynchrone Ereignisse Ereignisse verschiedener Instanzen werden durch Nachrichten geordnet Eine Nachricht muss erst gesendet werden, bevor sie verbraucht wird Ordnungsrelationen Beispiel: out(m2) < in(m2), out(m4) < in(m4), in(m1) < out(m2) < in(m4) < out(m5), in(m2) < out(m3) < out(m4), einschließlich der transitiven Hülle Protocol Engineering Wintersemester 2013/14 II.1/75 © Prof. Dr. H. König Nachrichten Nachrichten DTx DTy Überholen von Nachrichten Verlust von Nachrichten Finden von Nachrichten z.B. verspätete Nachrichten Protocol Engineering Wintersemester 2013/14 II.1/76 © Prof. Dr. H. König Timer t(0,100) Start Timer Stop / Reset Timer Time-out Protocol Engineering Wintersemester 2013/14 II.1/77 © Prof. Dr. H. König Bedingungen Bedingungen dienen der Beschreibung von Systemzuständen oder Vorbedingungen. Systemzustände shared all globale Zustände, die für alle Instanzen gelten shared Zustände, die nur von einigen Instanzen angenommen werden lokale Zustände Globale und geteilte Zustände können in verschiedenen MSCs enthalten sein !!! Zustände, an denen MSCs enden und andere beginnen !!! Protocol Engineering Wintersemester 2013/14 II.1/78 © Prof. Dr. H. König MSC für den XDT-Verbindungsaufbau msc XDT-Verbindungsaufbau Systemzustand XS XR CONNECT XDATrequ Vorbedingung when sequ=1 DT(sequ=1) XDATind ACK XDATconf DATA TRANSFER Protocol Engineering Wintersemester 2013/14 II.1/79 © Prof. Dr. H. König Instanzen-Erzeugung msc XS Sender XDATconf ~ ~ create ack_handler ACK ~ ~ ~ ~ Beenden einer Instanz Protocol Engineering Wintersemester 2013/14 II.1/80 © Prof. Dr. H. König B) Inline-Ausdrücke Protocol Engineering Wintersemester 2013/14 II.1/81 © Prof. Dr. H. König Inline-Ausdrücke Mit Hilfe von Inline-Ausdrücken können Teilabläufe kombiniert werden, um komplexere Abläufe zu beschreiben. loop - Zyklus opt - wahlweise Ausführung exc - Ausnahmebehandlung alt - Ausführungsalternativen par - parallele Ausführung Protocol Engineering Wintersemester 2013/14 II.1/82 © Prof. Dr. H. König MSC für vollständigen XDT-Verbindungsaufbau (Dienstspezifikation) msc XDT-Verbindungsaufbau Sender XDT-Diensterbringer XDATrequ alt Empfänger Erfolgereicher Verbindungsaufbau CONNECT XDATind XDATconf DATA_TRANSFER Abgelehnter Verbindungsaufbau XABORTind CONNECT Protocol Engineering Wintersemester 2013/14 II.1/83 © Prof. Dr. H. König MSC für vollständigen XDT-Verbindungsaufbau (Protokollspezifikation) msc XDT-Verbindungsaufbau Sender XS Y-Sender Y-Empf. XR Idle Empfänger Idle XDATrequ DT t Y-DT DT Await ACK XDATconf ACK ACK Y-DT Connected Protocol Engineering Wintersemester 2013/14 XDATind Connected II.1/84 © Prof. Dr. H. König C) High-level MSC Protocol Engineering Wintersemester 2013/14 II.1/85 © Prof. Dr. H. König High-level MSC High-level MSC ermöglichen es MSCs zu komplexeren oder gar kompletten Beschreibungen von Protokollen/Systemen zu kombinieren. Referenzen auf einzelne MSC Start-/Stopp-Symbole Um eine vollständige Beschreibung mit HMSC zu erhalten, müssen alle möglichen Kommunikationsabläufe miteinander kombiniert werden !!! kann sehr komplex werden !!! Protocol Engineering Wintersemester 2013/14 II.1/86 © Prof. Dr. H. König High-level MSC MSCReferenz Start Idle Verbindungsaufbau erfolglos Verbindungsaufbau erfolgreich Connected Datenübertragung Stopp Protocol Engineering Wintersemester 2013/14 II.1/87 © Prof. Dr. H. König
© Copyright 2025 ExpyDoc