Tele Entwurf von Telekommunikationssystemen- 60 - Übersicht 1. Einführung in den...

Entwurf von Telekommunikationssystemen - 1 - tele

Übersicht

1. Einführung in den Software-Entwurfsprozess

2. Anforderungsspezifikation mit Zustandsmaschinen

3. Anforderungsspezifikation mit Linearer Temporaler Logik

4. Automatenbasiertes Model Checking

5. Die Modellierungssprache Promela und der SPIN Model Checker

6. Effizienzsteigernde Massnahmen

7. Anwendungsbeispiele von SPIN Model Checking

8. Eine visuelle Entwicklungsumgebung für Promela/Spin

9.Verwandte, semi-formale Modellierungsmethoden


Zustandsorientierte Analyse

Zustand ein System besitzt unterschiedliche Variablen, die entweder sichtbar

oder intern und damit nicht sichtbar sein können jede Variable ist über einem Datenbereich definiert ein Zustand ist eine Funktion, die jeder Variable einen Wert aus dem

jeweiligen Datenbereich zuweist

Naheliegend, das Verhalten reaktiver Systeme durch Zustände, die Zustandswechsel hervorrufenden Stimuli und die durch Zustandswechsel hervorgerufenen Ereignisse zu charakterisieren



Analyseansatz nach [Davis] Definition von Objekten, Funktionen und Zuständen Beschränkung und Kontrolle der mit Objekten, Funktionen und

Zuständen assoziierten Aktionen Definition der Zusammenhänge von Objekten, Funktionen und

Zuständen

Objekte“… is a real-world entity, important to the discussion of requirements,

with a crisply defined boundary.” Charakterisiert durch

– Attribute– Funktionen– Zustände– Beziehung zu anderen Objekten

BeispielDas System soll den Typ der Sensoren an Bord jedes Schiffes

anzeigen.



Funktionen“… a task, service, process, mathematical function or activity that is

either (1) now being performed in the real world, or (2) to be performed by the system to be specified.”

BeispielDas System soll den Typ der Sensoren an Bord jedes Schiffes

anzeigen.Die Telefonanlage soll innerhalb von 100 ms einen Wählton

erzeugen Charakterisiert durch

– Das Objekt, das diese Funktion ausführt– Attribute der Funktion– Zustände, in denen die Funktion ausführbar ist– Verhältnis zu anderen Funktionen


Zustandsorientierte Analyse Zustand

“... is a condition of some thing that captures some history of that thing and is used by that thing to help to determine how it is to behave in certain circumstances.”

BeipieleSolange die Fahrwerksräder sich nicht drehen soll der

Umkehrschub nicht aktiv seinWaffen sollen nicht abgefeuert werden können solange sich das

Flugzeug im Trainingsmodus befindetWenn bei nicht läutendem Telefon der Hörer abgenommen wird

dann soll entweder ein Besetztzeichen ertönen und der Hörer wieder aufgelegt werden, oder es soll ein Wählton ertönen und eine Telefonnummer eingegeben werden können.

Charakterisiert durch– das Objekt, dem der Zustand gehört (jedes aktive Objekt hat

genau einen aktuellen Zustand)– Attribute eines Zustands– die in einem Zustand ausführbaren Funktionen– Zusammenhang mit anderen Zuständen


Beispiel: TelefonWenn bei nicht läutendem Telefon der Hörer abgenommen wird dann

soll entweder ein Besetztzeichen ertönen und der Hörer wieder aufgelegt werden, oder es soll ein Wählton ertönen und eine Telefonnummer eingegeben werden können.

Objekte– Benutzer

Attribute* Name etc. (hier nicht relevant)

Funktionen * hörer_abnehmen* hörer_auflegen* telefonnummer_wählen

Zustände* still* abgenommen* gewählt

Beziehungen* mehrere Benutzer teilen ein Telefon




Objekte– Telefon

Attribute* Nummer etc. (hier nicht relevant)

Funktionen * starte_ / stoppe_läuten* starte_ / stoppe_wählton* starte_ / stoppe_besetztton

Zustände* still* abgenommen* erwarte_nummer

Beziehungen* mehrere Benutzer teilen ein Telefon* Telefon wird mit anderem Telefon verbunden




Funktionen (hier unvollständige Aufstellung)– starte_wählton

Objekt: Telefon Attribute: - Zustände: abgenommen andere Funktionen: - (nicht gleichzeitig stoppe_wählton)

– telefonnummer_wählen Objekt: Benutzer (Telefon) Attribute: Nummer Zustände: abgenommen

– hörer_auflegen Objekt: Benutzer (Telefon) Zustände: abgenommen, erwarte_nummer


Beispiel: Telefon Zustände (hier unvollständige Aufstellung)

– abgenommen Objekt: Benutzer Attribute: Wählton oder Besetzton ertönt Funktionen: hörer_auflegen, telefonnummer_wählen Zusammenhang:

* Vorgängerzustand: still* Nachfolgezustand: gewählt (bei telefonnummer_wählen),

still (bei hörer_auflegen)– abgenommen

Objekt: Telefon Attribute: - Funktionen: starte_wählton, starte_besetztton Zusammenhang:

* Vorgängerzustand: still* Nachfolgezustand: erwarte_nummer (bei starte_wählton),

still (bei starte_besetztton)


Zustandsmaschinen

Reaktive Systeme sind charakterisiert durch Folgen von Zustandsübergängen, hervorgerufen durch Ereignisse, und begleitet von Antworten Zustandsübergänge (Transitionen) sind momentan und diskret während das System in einem Zustand ist, bleiben die Werte aller

Variablen konstant

Beschreibung durch Folgen von Zuständen und Zustandsübergängen


Zustandsmaschinen

Beschreibung durch Endliche Zustandsmaschine (finite state machine, FSM) Zustände

– momentaner Kontrollzustand– Werte aller diskreten Zustandsvariablen

ZustandstransitionsregelnVorher:

1. Kontrollzustand, in dem sich das System vor Ausführung der Transition befinden muss

2. Bedingung für die Auführbarkeit der Transition (Ereignis aus der Umgebung, Boolscher Ausdruck auf den Zustandsvariablen, true)

Nachher:3. optionale Änderung der Umgebung (meist Ausgabeereignis)4. Neuer Kontrollzustand


Zustandsmaschinen

Beispiel: Getränkeautomat (GA)

Zustand Eingabe Ausgabe Nachfolgezustand

frei g - erh

erh a - ausg

ausg (true) d frei

ausg (true) z frei

frei ausgerh?g ?a

!d

!z


Zustandsmaschinen

Endliche Zustandsmaschinen sei

Q: endliche Menge von Zuständenq0 Q (genannt Anfangszustand)I: ein Alphabet (genannt Eingabesymbole)O mit I O : ein Alphabet (genannt Ausgabesymbole)A = I O (genannt Ereignisalphabet): Q Q eine Relation: Q x A Q eine Relation: Q x I O x Q eine Relation

(Q, q0, ) nennen wir ein Transitionssystem

frei ausgerh


Zustandsmaschinen



(Q, q0, A, ) nennen wir eine endliche Moore-Maschine

frei ausgerh?g ?a

!d

!z


Zustandsmaschinen



(Q, q0, I, O, ) nennen wir eine endliche Mealey-Maschine

frei erh?g/-

?a/!d

?a/!z


Über Zustandsmaschinen

Moore und Mealey Machines haben die gleiche Ausdrucksfähigkeit (siehe [Hopcroft and Ullman])

Die hier betrachteten Zustandsmaschinen sind nichtdeterministisch, d.h., in einem Zustand können mehr als eine Transition zu unterschiedlichen Nachfolgezuständen gleichzeitig ausführungbereit sein


Zustandsmaschinen und Anforderungen

Beschreiben Zustandsmaschinen ein was oder ein wie?

Wie können Zustandsmaschinen Anforderungen spezifizieren?

implementierter

GA

Zustandsmaschinen

Spezifikation

GA

1

0

g a z g a d g a

frei ausgerh?g ?a

!d

!z





implementierter

GA

Zustandsmaschinen

Spezifikation

GA

1

0

g a z g a d g a g a d g a z g a z g a d g a z d g

frei ausgerh?g ?a

!d

!z





implementierter

GA

Zustandsmaschinen

Spezifikation

GA

1

0

d g a z d g a z g a d a g a d g a z g a z g a d

frei ausgerh?g ?a

!d

!z



A = {g, a, d, z} beschreibt ein Alphabet der extern beobachtbaren Ereignisse

Die Zustandsmaschine GA beschreibt ein mathematisches Modell für alle zulässigen Folgen beobachtbarer Ereignisse

Akzeptierungskriterien ist <g, a, d, g> eine zulässige Ereignisfolge ? ist <g, a> eine zulässige Ereignisfolge ? Notwendigkeit, Zustandsmaschinenmodell um Akzeptierungskriterien

zu erweitern

frei ausgerh?g ?a

!d

!z


Nichtdeterministische Endliche Automaten

EASei M = (Q, q0, A, ) eine endliche Zustandsmaschine, und F Q (wir nennen F die Menge der Akzeptierungszustände).Dann nennen wir N = (M, F) einen nichtdeterministischen endlichen

Automaten (EA).

PfadSei N ein EA. Wir nennen die Zustandsfolge (q0, q1, .. , qk) einen Pfad von N genau

dann, wenn

)))q),a,q)(((Aa((q 1iii

1k

0i



PfadmarkierungSei N ein EA. Wir nennen das Wort a = (a0, a1, .. , ak) A* eine Pfadmarkierung

von N genau dann, wenn es einen Pfad (q0, q1, .. , qk+1) von N gibt so dass

Ferner nennen wir a akzeptiert, falls qk+1 F. Bemerkung: Für jede von einem nichtdeterministischen EA

akzeptierte Sprache gibt es einen deterministischen EA, der die gleiche Sprache akzeptiert (siehe [Hopcroft and Ullman])

))q),a,q(((a 1iiii

k

0i



Akzeptierer für formale Sprachen Für GA, F = {frei} GA akzeptiert die Sprache LGA = (g a (z | d))* LGA repräsentiert vollständig alle zulässigen, beobachtbaren

Ereignisfolgen für GA

frei ausgerh?g ?a

!d

!z


Warum Endliche Automaten?

Warum nicht eine allgemeine Programmiersprache?

frei ausgerh?g ?a

!d

!z

main (){ ...frei: c = nextevent();switch(c) { case ‘g’: goto erh; default : goto blockiert }erh: c = nextevent();switch(c) { case ‘a’: goto ausg; default : goto blocking; }ausg: c = nextevent();switch(c) { case ‘d’: goto frei; case ‘z’: goto frei; default : goto blocking; }blocking: ...}


Warum Endliche Automaten?

Warum nicht eine allgemeine Programmiersprache? Welche Sprache (C, C++, Java, XML, ...)? Gefahr der Vorbestimmung einer Implementierung (implementation

bias)– Interessiert daran, was, nicht wie, zu spezifizieren– Keine gültige Implementierung soll ausgeschlossen werden

Die meisten Progammiersprachen besitzen keine (allgemein anerkannte) formale Semantik


Beschränkungen von Zustandsmaschinen

B1: Fehlende Datenabstraktion Variablen, Zähler nicht vorhanden Resultat

– Daten müssen in den Zustandsraum hineincodiert werden– Folge: enorme Komplexität des Zustandsraums



B1: Fehlende Datenabstraktion Variablen, Zähler nicht vorhanden Resultat

– Daten müssen in den Zustandsraum hineincodiert werden– Folge: enorme Komplexität des Zustandsraums



B2: Zustandsexplosion bei nebenläufiger Komposition Beispiel: Producer-Consumer System ([Ghezzi])

Copyright © Prentice-Hall, 1993



B2: Zustandsexplosion bei nebenläufiger Komposition Nebenläufige Komposition durch Bildung des kartesischen Produktes

der einzelnen Zustandsräume Annahme

– n Systemkomponenten– jede der i = 1, .., n Systemkomponenten hat k Systemzustände

Grösse des Zustandsraums des komponierten Systems:

Konsequenz: Wachstum exponentiell in der Anzal nebenläufiger Komponenten

“state explosion problem”

n

1iik


Beschränkungen von Zustandsmaschinen B3: Beschränkter Speicherplatz

Endliche Zustandsmaschinen haben nur endlichen Speicherplatz, daher können sie nur bis zu konstanten, endlichen Zahlen zählen

Problem zum Beispiel bei der Modellierung von Kommunikationskanälen: Grösse der Puffer

Bei der Spezifikation müssen diese Konstanten a priori bekannt sein implementation bias

B4: Fehlende Abstraktion/Verfeinerung Zustände und Transitionen können nicht verfeinert werden

B5: Fehlende Kompositions- und Synchronisationsmechanismen für nebenläufige Systeme Instanziierung / Terminierung von nebenläufigen Komponenten Kommunikation

– Broadcast oder Punkt-zu-Punkt– Warteschlangen oder Kanäle

Synchronisation– synchron oder asynchron


Beschränkungen von Zustandsmaschinen B6: Akzeptierer für endliche Ausführungfolgen

GA Beispiel akzeptiert LGA = (g a (z | d))* Reaktive Systeme: unendliche Ausführungsfolgen Benötigt: LGA = (g a (z | d))

B7: Mangel and Echtzeit-Ausdrucksfähigkeit “Wenn nach der Eingabe des Geldes der Benutzer nicht innerhalb

von 15 Sekunden das Getränk ausgewählt hat, wird das eingeworfene Geld zurückgegeben.”

B8: Graphische Repräsentierbarkeit Für komplexe Systeme ist es unmöglich, sie mit Hilfe von

Zustandsmaschinen darzustellen Konsequenz einiger der Bns


Erweiterungen B1 (Datenabstraktion)

Erweiterte Endliche Zustandsmaschinen (Extended Finite State Machines, EFSMs)

B2 (Zustandsexplosion) Dekomposition in Menge von kommunizierenden

Zustandsmaschinen (CFSMs) EFSMs

B3 (Beschränkter Speicher) EFSMs

B4 (Abstraktion / Verfeinerung) Hierarchische Zustandsmaschinen (HFSM, Statecharts)

B5 (Mechanismen für nebenläufige Systeme) Komposition von CFSMs

B6 (Unendliche Ausführungfolgen) Automaten auf unendlichen Eingaben (Büchi Automaten)

B7 (Echtzeitanforderungen) zeitbeschränkte FSMs, Timer-Konstrukte

B8 (Graphische Repräsentierbarkeit)


Kommunizierende Zustandsmaschinen (CFSMs) Nach [Brand and Zafiropulo] (IBM Forschungslabor Zürich)

Ansatz nebenläufige FSMs (2) + Kommunikationskanäle (=“Protokoll“) jede FSM repräsentiert einen nebenläufigen, kommunizierenden

Prozess mit einer endlichen Anzahl von Kontrollzuständen jeder Kommunikationskanal ist

1. voll-duplex,2. fehlerfrei,3. hat eine first-in-first-out Bedienstrategie,4. und hat unbeschränkte Kapazität(1. - 3. charakterisiert einen perfekten voll-duplex Kanal)Frage: wie modelliert man imperfekte Kanäle?

ein Paar Kanäle (cij und cji) für jedes Paar (i, j) von Maschinen

M1

M2 M3


Kommunizierende Zustandsmaschinen (CFSMs)

Formalisierung N: eine positive ganze Zahl i, j = 1, .. N: Index der Prozesse : N disjunkte, endliche Mengen, Qi bezeichnet die

Zustandsmenge des Prozesses i

: N diskunkte Mengen mit (i)(Aii = ), Aij bezeichnet den Nachrichtenvorrat (Alphabet) für den Kanal von i j

: Relation, die für jedes Paar i, j die folgenden Abbildungen bestimmt

Q x A Q

Q x A Q

: Tupel von Anfangszuständen,

Definition Wir nennen ein Protokoll

N

1iiQ

N

1j,iijA

0iq i0

i Qqi

,A,q,Q ij0ii



Notation s Q: der Zustand des Prozesses i x A: eine Nachricht

– ?x Empfang einer Nachricht– !y Senden einer Nachricht

f((s, .., s)) = (f(s), .., f(s)) x, y: Nachrichten X, Y: Folgen von Nachrichten x, xy, xY, xXY: verkettete Nachrichtenfolgen



Ein Server-Protokoll (nach [Brand and Zafiropulo) Initially, both processes user and server are in states ready and idle,

respectively. The user can send a request by a message REQ to the server, which enters state service after receiving REQ. When finished processing the request, the server sends a message DONE to the user and goes back to state idle. Afer sending REQ, the user enters the wait state and returns to ready when receiving DONE. In state idle, the server indicates a fault to the user by sending an ALARM message. The user registers the fault and sends the server an ACK message. Upon receipt of ACK, the server returns to state ready.

ready

wait reg

idle

service fault

!REQ

?DONE!ACK

?ALARM ?REQ

!DONE?ACK

!ALARM

user server


Kommunizierende Zustandsmaschinen (CFSMs) Alternating Bit Protokoll (siehe z.B. [Holzmann 91])

einfaches Protokoll zur Sicherung unzuverlässiger Datenkanäle sender sendet mit einer Sequenznummer n, n {1, 2}, Nachricht msgn receiver bestätigt mit ackn sender setzt neue Sequenznummer auf 1 + n mod 2 bei Empfang falscher Sequenznummer erneute Übertragung symmetrische Variante existiert

!msg1

?ack0?ack1

?ack1 !msg0

?ack0

sender

?msg1!ack1

?msg0!ack0

receiver

s1

s2

r0

r1 r2



Semantik eines Protokols? Folge der zulässigen Zustandssequenzen

Zustand eines Protokolls? Summe von

– dem lokalen Zustand jeder der 1 .. N Prozesse, und– dem Zustand aller Kanäle c A*

jedes c entspricht einer Sequenz von gesendeten, aber noch nicht empfangenen Nachrichten

Wir nennen dies den globalen Systemzustand



Wie erhalten wir die Berechnungen eines Protokolls, d.h., Sequenzen globaler Systemzustände? Anfänglich: alle Prozesse in und alle c = Zustandstransitionen durch Sende- oder Empfangsereignisse

hervorgerufen– Sendeereignis

füge Nachricht am Ende der entsprechenden Nachrichtenwarteschlange (= Kanal) an

verändere den lokalen Systemzustand des sendenden Prozesses

– Empfangsereignis entnehmen die zu empfangende Nachricht dem Kopf der

Nachrichtenwarteschlange verändere den lokalen Systemzustand des empfangenden

Prozesses Führt in neuen globalen Systemzustand

0iq



Definition Globaler Systemzustand Sei

– ein Protokoll– S = (S, .. ,SN) ein N-Tupel von Zuständen – C ein N Tupel

so dass für alle i, j: c A* Wir nennen (S, C) einen globalen Systemzustand

,A,q,QP ij0ii

N

1

N1

c

c

cc

C



Definition Zustandstransitionsrelation Sei P ein Protokoll und G = {(S, C) | (S, C) ein globaler

Systemzustand ist} |— : G G wird wie folgt definiert

(S, C) |— (S’, C’) gdw i, k, x so, dass entweder a) (S, C) und (S’, C’) identisch bis auf die folgenden

Ausnahmen sinds’ = (s, !x) (senden durch i)c’ = cx

oderb) (S, C) und (S’, C’) identisch bis auf die folgenden

Ausnahmen sinds’ = (s, ?x) (empfangen durch k)c = xc’



Definition Erreichbarer Systemzustand Sei

– G der Anfangszustand eines Protokolls,– G ein globaler Systemzustand des gleichen Protokolls,– |— die Zustandstransitionsrelation dieses Protokols, und

bezeichne |—* die transitive Hülle von |—. Wir sagen dass G erreichbar ist falls gilt

G |—* G

Pfade, Pfadmarkierungen und die akzeptierte Sprache können mit Hilfe von |— wie für EA definiert werden



Modellierung von Nebenläufigkeit CFSM Modell modelliert lineare Folgen globaler Systemzustände

(siehe entweder .. oder Konstrukt in der Definition von |—) Wie modelliert man, dass zwei Zustände oder Ereignisse nebenläufig

sind? Annahme: falls zwei Ereignisse E und E nebenläufig sind, dann

geht man davon aus, dass jede Reihenfolge dieser Ereignisse möglich sein muss, also in der Menge der erlaubten Ausführungsfolgen für das System enthalten sein muss:

{<…, E, …, E, …>, <…, E, …, E, …>, …} Interleaving Semantics



Ausdrucksfähigkeit CFSMs sind Turing-vollständig

– Beweisidee: drei Prozesse: P1, P2, P3, simuliere die Kontrolle der TM in der Zustandsmaschine von

P2 benutze P1 und die Kanäle c und c um das linke, und P3

und c und c um das rechte Bandende zu simulieren wichtig: alle c haben unbeschränkte Länge

Konsequenzen– unbeschränkter Raum globaler Systemzustände– unentscheidbare Probleme:

Termination wird ein Kommunikationsereignis jemals ausgeführt? ist ein Systemzustand erreichbar? ist das Protokoll frei von Deadlocks? gibt es eine obere Schranke für die Länge der c?



Ausdrucksfähigkeit Ein Kanal c ist beschränkt, falls es eine Konstante h gibt, so dass

für jeden erreichbaren globalen Systemzustand (S, C) c eine Sequenz mit einer maximalen Länge von h ist.

– für beliebige Protokolle ist Beschränktheit eines Kanals untentscheidbar

– für viele praktische Protokolle sind einzelne oder alle Kanäle beschränkt

Die oben genannten Erreichbarkeits- und Deadlockprobleme sind für Protokolle, bei denen alle Kanäle beschränkt sind, entscheidbar

Konsequenz– endliche Approximation – Einführung von CFSM-Modelle mit beschränkten Kanälen zur

vollständigen formalen Analyse Gefahr der Einführung von Deadlocks


-Automaten

Akzeptierungskriterium für NEA Ein EA akzeptiert ein Wort a A* genau dann, wenn der Automat

beim einlesen dieses Wortes nach einer endlichen Anzahl von Schritten in einem Akzeptierungszustand hält

Reaktive Systeme sind durch unendliche Ereignis- und Zustandsfolgen gekennzeichnet

Akzeptierungskriterium für a A ?

Büchi Automat Definition wie EA Akzeptierungskriterium

– Eine unendliche Folge a A wird von einem Büchi Automaten akzeptiert, falls der Automat beim Einlesen von a unendlich häufig durch mindestens einen der Zustände in der Menge der Akzeptierungszustände F läuft

frei ausgerh?g ?a

!d

!z


-Automaten

Büchi-Automat sei

Q: endliche Menge von Zuständenq0 Q (genannt Anfangszustand)A ein Endliche Menge von Ereignissymbolen (genannt

Ereignisalphabet): Q x A Q eine RelationF Q (genannt Akzeptierungsmenge)

wir nennen M = (Q, q0, A, , F) einen Büchi-Automaten

Akzeptierungskriterium Sei = s, s, … eine Sequenz, dann

[i] = s– || bezeichnet die Länge von ( falls unendlich)


-Automaten

Akzeptierungskriterium Sei = s, s, … eine Sequenz, dann

[i] = s– || bezeichnet die Länge von ( falls unendlich)

Sei

– eine Sequenz von Ereignissen– eine Sequenz von Zuständen von M

Wir sagen, dass ein Lauf auf ist, gdw. [0] = q, und– (i: 0 i ||)([i] ([i-1], [i-1]))

Sei M() = { | ist ein Lauf auf } – INFM() = {q Q | q erscheint unendlich häufig in jedem Element

von M()} wird von M akzeptiert falls

INFM() F

AM

QM

AM


-Automaten

Beispiel Anforderung

Wann immer ein a beobachtet wird, kann irgendwann später auch ein b beobachtet werden

Übersetzung in AusführungfolgenIn jeder Ausführungsfolge von M (in jedem Wort aus ) muss jedes

Vorkommen von a von einem Vorkommen von b gefolgt werden

Kommunikations-

medium

MSender Emgfänger

a b

(=DATreq) (=DATind)

AM

S1 S2

a

b

b, c a, c

Q = {S1, S2}, q = S1, F = {S1}


-Automaten

Akzeptanz endlicher Aufsührungsfolgen durch Büchi Automaten Annahme: der letzte Zustand wird unendlich häufig wiederholt


-Automaten

Beispiel Falls die Selbsttestroutine des Getränkeautomaten einen Fehler

entdeckt, dann wird das bereits eingegebene Geld zurückgegeben und der Automat verbleibt dauerhaft in einem Zustand in dem die Anzeige “sorry, out of order” erscheint.

F = {frei, sorry}

frei ausgerh?g ?a

!d

!z

fehler

sorry

!z

*

?f

?f?f


-Automaten Literatur

[Thomas] [Alpern and Schneider]


Erweiterte Endliche Zustandsmaschinen (EFSMs)

Eine EFSM ist eine FSM erweitert um Datenabstraktion (Variablen) Operationen auf Variablen symbolische (explizite) Zustände Boole’sche Tansitionsbedingungen


Erweiterte Endliche Zustandsmaschinen (EFSMs)

Formalisierung S: Menge der symbolischen Zustände D: n-dimensionaler linearer Raum, jedes D ist ein Datenbereich V = {, v, .., v}: endliche Menge von Programmvariablen

: Kontrollvariable über Domäne S– V = (v, .., v) D: Datenvariablen

O: endliche Menge von Ausgabesignaltypen I: endliche Menge von Eingabesignaltypen T: S x 2 x I S x 2 x O C: eine Anfangsbedingung über S x 2

Wir nennen E = (S, D, V, O, I, T, C) eine erweiterte endliche Zustandsmaschinen (EFSM)

Bemerkungen Zustand ist eine Funktion s: V 2 x 2 Da die D potentiell unendlich sind haben EFSM potentiell eine

unendliche Zustandsmenge EFSM sind Turing-vollständig

DD

D

S D


CEFSMs

Kommunizierende Erweiterte Zustandsautomaten Grundlage für viele praktische Spezifikationssprachen

– Specification and Description Language (SDL) standardisiert nach ITU Z.100

– Estelle ISO standardisiert

– ROOM / UML RT– Promela (mit endlicher Kanalkapazität)


Hierarchische Zustandsmaschinen (HFSM)



Grundkonzepte Zustandsabstraktion und Verfeinerung

– geometrischer Einschluss Higraphs (s. [Harel 88])

– Kombinieren Konzepte von Venn-Diagrammen (geometrisches Umfassen) Hypergraphen (Kanten verbinden mehr als zwei Knoten)

Multi-level transitions– z.B.: S1- scan_digits - S2

Gruppentransitionen– z.B.:S4 - S1

Statecharts Notation (s. [Harel 87])– Zustandsdiagramme– Tiefe– Orthogonalität (nebenläufige Komposition von Zuständen)– Broadcast-Kommunikation

HCEFSM: ROOM/UML RT



HCEFSM-basierte CASE Werkzeuge

URLs iLogix: www.ilogix.com Rational: www.rational.com ObjecTime: www.objectime.com


Zusammenfassung: Erweiterungen von FSMs B1 (Datenabstraktion)

Erweiterte Endliche Zustandsmaschinen (Extended Finite State Machines, EFSMs)

B2 (Zustandsexplosion) Dekomposition in Menge von kommunizierenden

Zustandsmaschinen (CFSMs) EFSMs

B3 (Beschränkter Speicher) EFSMs

B4 (Abstraktion / Verfeinerung) Hierarchische Zustandsmaschinen (HFSM, Statecharts)

B5 (Mechanismen für nebenläufige Systeme) Komposition von CFSMs

B6 (Unendliche Ausführungfolgen) Automaten auf unendlichen Eingaben (Büchi Automaten)

B7 (Echtzeitanforderungen) zeitbeschränkte FSMs, Timer-Konstrukte

B8 (Graphische Repräsentierbarkeit)


Bibliographische Referenzen

[Alpern and Schneider] B. Alpern and F. Schneider, Recognizing Safety and Liveness, Distributed Computing, 2:117-126, 1987

[Brand] D. Brand and P. Zafiropoulo, On Communicating Finite State Machines, Journal of the ACM (20) 2, April 1983, S. 323-342

[Ghezzi] C. Ghezzi et al., Fundamentals of Software Engineering, Prentice-Hall, 1993

[Harel 87] D. Harel, Statecharts: A Visual Formalism for Complex Systems, Science of Computer Programming 8 (1987), S. 231-274

[Harel 88] D. Harel, On Visual Formalisms, CACM, Volume 31, Number 5, S. 514-530


Bibliographische Referenzen

[Holzmann 91] G. Holzmann, Design and Validation of Computer Protocols, Prentice-Hall, 1991

[Hopcroft and Ullman] J. Hopcroft and J. Ullman, Introduction to Automata Theory, Languages, and Computation, Addison-Wesley, 1979

[Thomas] W. Thomas, Automata on Infinite Objects, in: J. van Leeuwen (ed.), Handbook on Theoretical Computer Science, Vol. B, Elsevier, 1990

Tele Entwurf von Telekommunikationssystemen- 60 - Übersicht 1. Einführung in den...

Documents

Transcript of Tele Entwurf von Telekommunikationssystemen- 60 - Übersicht 1. Einführung in den...