PE Kap 2.1 - Protocol Engineering

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 tT ist definiert durch das Tupel <s,c,i,o,s',c'>, wobei
sS den aktuellen Zustand, cC den Kontext vor Ausführung der
Transition, iI eine Eingabe, oO 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

Download Report