tele entwurf von telekommunikationssystemen- 141 - Übersicht 1. einführung in den...
TRANSCRIPT
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
Entwurf von Telekommunikationssystemen - 2 - tele
Logik für Temporale Anforderungen
Büchi-Automaten repräsentieren einen operationellen Ansatz zur Beschreibung temporaler Anforderungen an reaktive Systeme
Idee: Verwendung von Logiken als abstrakter, deskriptiver Ansatz zur Spezifikation temporaler Anforderungen (s)((s(a) ((s | i j)(s(b))))
– explizite Quantisierung über Zustandssequenzen
S1 S2
a
b
b, c a, c
Q = {S1, S2}, q = S1, F = {S1}
Entwurf von Telekommunikationssystemen - 3 - tele
Modallogik Die Wahrheit von elementaren Propositionen und von
Teilformeln wird mit Modalitäten versehenLp: „es ist notwendig, dass p wahr ist“Mp: „es ist möglich, dass p wahr ist“Lp: „es ist nicht notwendig, dass p wahr ist“Mp: „es ist unmöglich, dass p wahr ist“
Formeln der Modallogik Sei eine Menge atomarer Propositionen und sei p in , dann gilt:
– p ist eine Formel– falls eine Formel ist, dann ist eine Formel– falls und Formeln sind, dann sind auch
(Implikation) (Äquivalenz)L M
Formeln
Entwurf von Telekommunikationssystemen - 4 - tele
Modallogik Interessante Fragen
Lp p ? Lp Mp ? Mp Lp ? Notwendigkeit einer Semantikdefinition und Axiomatisierung
Modelle Modallogiken werden über semantischen Modellen interpretiert Die Struktur (mathematischen Eigenschaften) dieser Modelle
entscheidet darüber, welche der oben genannten Formeln gültig sind Für eine gegebene Instanz eines Modells kann der Wahrheitswert
einer modallogischen Formel bestimmt werden Sei eine Menge von atomaren Propositionen. Ferner, sei
– W eine Menge von Welten,– V W x W eine Sichtbarkeitsrelation auf den Welten, und– A: W x {wahr, falsch}, dann nennen wir (W, V, A) ein Modell oder eine Kripke-Struktur
Entwurf von Telekommunikationssystemen - 5 - tele
Modallogik
Interpretation der Modaloperatoren Lp: für alle sichtbaren Welten ist p wahr Mp: es gibt eine sichtbare Welt, in der p wahr ist
Struktur von R Reflexivität Transitivität
Beispiele In w ist Mp wahr In w ist Lp wahr, falls R nicht reflexiv ist In w ist Lq wahr, falls R nicht transitiv ist In w ist Mq wahr, falls R transitiv ist
pq
pq
pq
w w w
Entwurf von Telekommunikationssystemen - 6 - tele
Modallogik Modelltheoretische Semantik der Modallogik
Sei – M = (W, V, A) ein Kripke-Modell, eine Menge von atomaren Propositionen und p , – w und v W, – und und Formeln,
dann definieren wir die Relation (Erfüllungsrelation) für M wie folgt:
– (M, w) p gdw A(w, p) = wahr– (M, w) p gdw A(w, p) = falsch– (M, w) gdw (M, w) und (M, w) – (M, w) L gdw (v: (w, v) V)((M, v) )– (M, w) M gdw (v: (w, v) V)((M, v) )
Weiter definieren wir syntaktisch ( ) ( ) ( )M L
Entwurf von Telekommunikationssystemen - 7 - tele
Modallogik Axiomatisierung
A1. ( ) A2. ( )A3. ( ) ( )A4. ( ) (( ) ( ))A5. L A6. L( ) (L L)A7. L LLA8. M LM
Definition Theorem Wir nennen eine Formel , die von der Menge der Axiome abgeleitet
werden kann, ein Theorem und schreiben |— . Weitere Axiome
T1. |— und |— ( ) impliziert |— (modus ponens)T2. |— impliziert |— L
Entwurf von Telekommunikationssystemen - 8 - tele
Verhältnis Axiome - Sichtbarkeitsrelation A5 gdw R ist reflexiv
– L A7 gdw R ist transitiv
– L LL A6 gilt für jede beliebige Sichtbarkeitsrelation
– L( ) (L L) Systeme der Modallogik [Hughes and Cresswell]
A1- A6 T1, T2: System T System T, A7: System 4 System 4, A8: System 5
Systeme T, 4 und 5 verfügen über eine widerspruchsfreie und vollständige Aximatisierung
Modallogische Formeln können daher für ein bestimmtes System gültig und für ein anderes ungültig sein
Modallogik
Entwurf von Telekommunikationssystemen - 9 - tele
Modallogik
Temporale Interpretation der Modallogik Welten entsprechen Systemzuständen Sichtbarkeitsrelation entspricht Folge der Systemzustände
– ein System sieht seinen aktuellen Zustand Reflexivität– Systemzustand s folgt auf s und s folgt auf s, dann folgt s
auf s Transitivität Temporale Logik ist eine Interpretation der Modallogik auf Basis der
System 4 Axiomatisierung Die Lineare Temporale Logik (LTL), die wir im folgenden betrachten,
basiert auf System 4.3.1 nach [Hughes and Cresswell] – neben Reflexivität und Transitivität gelten Konnektivität und
Diskretheit Für mehr Information über Modallogik siehe auch [Huth and Ryan]
Entwurf von Telekommunikationssystemen - 10 - tele
Temporale Prädikate P1
Wenn eine komplette, korrekte Telefonnummer gewählt worden ist, und der angerufene Teilnehmer nicht besetzt ist, und der Anrufer nicht bisher aufgelegt hat, dann wird der Angerufene irgendwann später einen Klingelton erhalten.
P2Wenn es bei dem Angerufenen klingelt und er den Hörer aufnimmt, dann wird irgendwann später die
Telefonverbindung hergestellt sein.
Zustandssequenz
Vollständige Spezifikation wird durch Konjunktion aller P gewonnengewählt ... besetzt, klingeln, aufnehmen ... verbunden
P1 P2
i
n
1i
PP
s s s
Entwurf von Telekommunikationssystemen - 11 - tele
Zustandssprache Zustandssprache ([Manna and Pnueli 1992])
Sei V ein Vokabular bestehend aus Variablennamen, und sei für jede Variable eine Domäne mit entsprechenden Ausdrücken für Funktionen und Operatoren definiert
Ausdrücke– jede Variable x V – Funktionsausdrücke der Form (e, ..., e) falls alle e, ..., e
Ausdrücke sind– Bsp.: x+3y, hd(q).x, A B
Atomare Formeln– jede Proposition x V– P(e, ..., e) falls P ein Prädikat über V– Bsp.: x > y+1, x A B
Zustandsformeln– jede atomare Formel– falls p, q atomare Formeln, dann sind
p, p q, p q, p q, p qZustandsformeln
Entwurf von Telekommunikationssystemen - 12 - tele
Zustandssprache
Semantik der Zustandssprache Zustand
– ein Zustand s über V ist eine Interpretation die jeder Variable u V ein Wert des jeweiligen Wertebereichs zuweist
– s[u] Modell
– Ein Modell über V ist eine unendliche Folge = s, s, ...
so, dass jedes s ein Zustand über V ist Ausdrücke
– s ist Zustand über V, e ein Ausdruck über V– s[e] (Auswertung von e im Zustand s) definiert durch
Wert von x V is s[x] für (e, ..., e) wird definiert durch
s[(e, ..., e)] = (s[e], ..., s[e])
Entwurf von Telekommunikationssystemen - 13 - tele
Zustandssprache Boolesche Formel in s (s[])
– für atomare Formeln P(e, ..., e)s[P(e, ..., e)] = P(s[e], ..., s[e])
– für boolesche Formeln, die durch boolesche Operatoren gebildet werden
s[p] = s[p]s[p q] = s[p] s[q] s[p q] = s[p] s[q] s[p q] = s[p] s[q]s[p q] = s[p] s[q]
– Beispiels[(x+z = 2y) (y > z)]
= (s[x]+s[z] = 2.s[y]) (s[y] > s[z])= ((0 + 2 = 2.1) (1 > 2))= wahr falsch= falsch
Entwurf von Telekommunikationssystemen - 14 - tele
Zustandssprache Erfüllung einer Formel durch einen Zustand
– sei s ein Zustand und p eine Zustandsformel– wir definieren die Relation s||=p durch
s ||= p gdw s[p] = wahrs ||= p gdw nicht s ||= ps ||= p q gdw s ||= p oder s ||= q
(die Regeln für die übrigen Booleschen Operatoren können abgeleitet werden)
Falls s ||= p sagen wir dass s ein p-Zustand ist
Entwurf von Telekommunikationssystemen - 15 - tele
Erfüllbarkeit und Gültigkeit
Zustands-Erfüllbarkeit p ist zustandserfüllbar, falls es einen Zustand s gibt, so dass s ||= p
Zustands-Gültigkeit p ist zustandsgültig, falls s ||= p für alle Zustände s
Beispiele Sei x eine ganze Zahl
– 0 < x < 2 ist zustandserfüllbar (0 < x < 1) ist zustandsgültig
Entwurf von Telekommunikationssystemen - 16 - tele
Temporallogik
Temporale FormelnSeien p, q Formeln der Zustandssprache p ist eine temporale Formel p, p, p, p U q und pW q sind temporale Formeln
Interpretation über Sequenzen Wir betrachten unendliche Sequenzen von Zuständen
= s, s, .., s, ... Wir definieren die Relation Erfüllungsrelation über
Zustandssequenzen und schreiben (, j) p falls die Sequenz an Position j die temporallogische Formel p erfüllt
Zustandsformeln(, j) p gdw s ||= p
Entwurf von Telekommunikationssystemen - 17 - tele
Temporallogik
Zustandsformeln(, j) p gdw s ||= p
Beispiel: p x = y
s s ss s s ...
p
x = 1 2 3 4 5 6 ...
y = 5 4 3 2 1 0 ...
f f w f f f
Entwurf von Telekommunikationssystemen - 18 - tele
Operatoren der Temporallogik
Next () Sei p eine temporallogische Formel (, j) p gdw. (, j+1) p Beispiel
p (x = y)
s s ss s s ...
p
x = 1 2 3 4 5 6 ...
y = 5 4 3 2 1 0 ...
f w f f f f ...
Entwurf von Telekommunikationssystemen - 19 - tele
Operatoren der Temporallogik
Henceforth () Sei p eine temporallogische Formel (, j) p gdw. (k: kj)(, k) p Beispiel
p x > 3
s s ss s s ...
p
x = 1 2 3 4 5 6 ...
f f f w w w ...
Entwurf von Telekommunikationssystemen - 20 - tele
Operatoren der Temporallogik
Eventually () Sei p eine temporallogische Formel (, j) p gdw. (k: kj)(, k) p Beispiel
p x = 4
Anmerkung– (, j) p impliziert (k: kj)(, k) p und sind duale Operatoren:
p pp p
s s ss s s ...
p
x = 1 2 3 4 5 6 ...
w w w w f f ...
Entwurf von Telekommunikationssystemen - 21 - tele
Operatoren der Temporallogik Until (U)
Seien p und q temporallogische Formeln (, j) p U q gdw.
(k: kj)((, k) q) und (i: j i < k)((, i) p) Beispiel
Anmerkung p wahr U p– p U q q
s s ss s s ...pUq
p w w w * * * ...
w w w w f f ...
q f f f w f f ...
Entwurf von Telekommunikationssystemen - 22 - tele
Operatoren der Temporallogik Unless (W) oder Weak Until
Seien p und q temporallogische Formeln (, j) p W q gdw.
(, j) p U q oder (, j) p Beispiel
Anmerkung p p W falsch– p W q p U q p
s s ss s s ...p w w w w w w ...
w w w w f f ...
q * * * * * * ...
pWq
s s ss s s ...p w w w * * * ...
w w w w f f ...
q f f f w f f ...
pWq
Entwurf von Telekommunikationssystemen - 23 - tele
Beispiele
Beispiele p q
– “ein p-Zustand am Anfang wird irgendwann von einem q-Zustand gefolgt”
(p q) p q – jedes Vorkommen von p wird irgendwann von q gefolgt– auch genannt “p leads-to q” (von Lamport eingeführt), z.B.
DATreq DATind (DATreq DATind)
p
* *
...
... q*
...
p
q
p
p p p
q q*
*
...
...
Entwurf von Telekommunikationssystemen - 24 - tele
Beispiele
Beispiele p
– “ hat unendlich viele p-Postitionen”
p – “ hat nur endlich viele p-Postitionen”
p pp p p pp p ...
p pp p p pp p p p p ...
Entwurf von Telekommunikationssystemen - 25 - tele
Beispiele
Beispiele (p q)
“Der Nachfolger jedes p-Zustands ist ein q-Zustand” (p p)
(p p)“Der Nachfolger jedes p-Zustands ist ein p-Zustand”“Einmal p, immer p”
Entwurf von Telekommunikationssystemen - 26 - tele
Erfüllung und Gültigkeit
Erfüllung Gegeben sei Zustandsfolge (oder Modell) und Formel p erfüllt die Formel p an Position i (oder s ist ein p-Zustand oder eine
p-Postition) falls (, i) p
erfüllt die Formel p (oder p gilt für ), falls (, 0) pund wir schreiben dann
p
Gültigkeit Eine Formel p ist eine gültige Formel falls gilt ()( p), und wir
schreiben dann p
Wir suchen nach gültigen Formeln der TL die es uns erlauben, Eigenschaften in anderer, äquivalenter Form nierderzuschreiben
Für Formeln p und q schreiben wirp q für (p q) (“entailment”)p q für (p q)
Entwurf von Telekommunikationssystemen - 27 - tele
Gültige Formeln
Entailment p p p U q (p q) p W q (p q) p p q p U q q p W q
Expansion p (p p) p (p p) p U q (q [p (p U q)]) p W q (q [p (p W q)])
Entwurf von Telekommunikationssystemen - 28 - tele
Gültige Formeln
Dualitäten p p p p (p U q) (q) W (p q) (p W q) (q) U (p q) p p
Starke und schwache Operatoren p U q (p W q q) p W q (p U q p) p U q p W q
Entwurf von Telekommunikationssystemen - 29 - tele
Gültige Formeln
IndempotenzZweifache Anwendung gleich einfacher Anwendung p p p p p U (p U q) (p U q) p W (p W q) (p W q) (p U q) U q (p U q) (p W q) W q (p W q)
Absorption p p p p Zusammen mit den Indempotez-Regeln kann man daher zeigen,
dass es für eine Formel p, die frei von temporalen Operatoren ist, nur 4 unterschiedliche unäre Modalitäten gibt:p, p, p, p
(Dies entspricht der “finite-model property” der System 4.3.1 Modallogik nach [Hughes and Cresswell])
Entwurf von Telekommunikationssystemen - 30 - tele
Gültige Formeln
Kommutativität mit (p) p (p q) p q (p W q) p W q
Distribution (p q) p q (p q) p q (p q) p q (p q) p q
Entwurf von Telekommunikationssystemen - 31 - tele
Basisoperatoren und Axiomatisierung
Mögliche Menge von Basisoperatoren, W, Abgeleitete Operatoren
p = p W falsch p = p = (p W falsch)– p U q = p W q q = p W q (p W falsch)
Mögliche Axiomatisierung p p p p (pq) (p q) (pq) (p q) p p (p p) (p p) p W q [q (p (p W q))] p p W q
Entwurf von Telekommunikationssystemen - 32 - tele
Eigenschaften
Eigenschaftsklassen in Temporaler Logik Verwendung der syntaktischen Form der Formeln Eine Eigenschaft wird durch eine Formel der Temporallogik
spezifiziert, falls über dem Zustandsvokabular definiert ist und die folgende Bedingung gilt:
gdw. bildet daher eine Entscheidungsmechanismus, der festlegt, ob eine
Zustandsfolge des Systems zu den zulässigen Zustandsfolgen gehört.
Safety-Prgress Klassifikation [Manna and Pnueli] Klassifikation orthogonal zu der Sicherheits-Lebendikgeits
Klassifikation
Entwurf von Telekommunikationssystemen - 33 - tele
Eigenschaften
Safety kanonische Form: p Eine Sicherheitseigenschaft (safety property) ist eine Eigenschaft, die
durch eine Sicherheitsformel ausgedrückt werden kann Beispiele:
(x > 0) ((y 2) W (x = 1)) = ((y = 2) (x = 1))
eventually in the past always in the past in the previous state(Diese Operatoren zählen an dieser Stelle nicht zu den
temporalen Operatoren, mit anderen Worten, sie können in Sicherheitsformeln vorkommen - mehr dazu in [Manna and Pnueli 92])
Entwurf von Telekommunikationssystemen - 34 - tele
Eigenschaften
Guarantee kanonische Form: p “einmalig, aber ohne Wiederholung garantiert” Beispiel:
((y = 2) (x = 1)) Dualität von Safety und Guarantee
p p p p
(p q gdw. p q ist eine wahre Formel)
Entwurf von Telekommunikationssystemen - 35 - tele
Eigenschaften
Obligation kanonische Formen (äquivalent)
– p q p q
“falls irgendwann p, dann auch irgendwann q” Beispiel:
(x = 1) (y = 2) Eigenschaften
– Jede Boolesche Kombination von Safety und Guarantee Eigenschaften ist eine Obligation Eigenschaft
– Die Klasse der (einfachen) Obligation Eigenschaften umfasst strikt die Klassen Safety und Guarantee:
p q kann weder als durch die ausschliessliche Verwendung von Safety noch durch die ausschliessliche Verwendung von Guarantee Formeln ausgedrückt werden.
Entwurf von Telekommunikationssystemen - 36 - tele
Eigenschaften
Response kanonische Form
p – “unendlich viele p-Positionen”
alternative Normalform (p q) = p q– “ein p wird immer von einem q gefolgt”
Beispiele: ((x = 1) (y = 2)) ([in!DATreq] [out?DATind])– für eine gegebene Transition :
(enabled() last_taken())“justice” (Gerechtigkeit): entweder wird unendlich häufig zurückgezogen oder wird unendlich häufig ausgeführt
Alle Safety und Guarantee Eigenschaften sind spezielle Fälle von Response-Formeln
Entwurf von Telekommunikationssystemen - 37 - tele
Eigenschaften
Persistence kanonische Form
p – “es gibt nur endlich viele nicht-p-Positionen”– benutzt zur Beschreibung der Stabilisierung eines Systems nach
endlich vielen Schritten Beispiele:
– (x = 1) (y = 2) ((x = 1) (y = 2))
Dualität von Response und Persistence p p p p
Entwurf von Telekommunikationssystemen - 38 - tele
Eigenschaften
Reactivity kanonische Form
p q Disjunktion einer Response und einer Persistence Formel Alternative Schreibweise
p q p q q p
Beispiel: (x = 1) (y = 2) enabled() last_taken()
“compassion” (Mitleid) oder “strong fairness” )starke Fairness: wenn unendlich häufig zur Ausführung bereit ist wird es auch unendlich häufig ausgeführt
Entwurf von Telekommunikationssystemen - 39 - tele
Eigenschaften
Safety-Progress Klassifikation
Entwurf von Telekommunikationssystemen - 40 - tele
Sicherheit und Lebendigkeit
Sicherheits- und Lebendigkeitsformeln Sicherheit
– Beispiel(receive sent)
– mit anderen Worten, man kann das Eintreten von etwas ungewolltem in endlicher Zeit erkennen
ist eine Sicherheitsformel, gdw. jede Sequenz , die verletzt (die also erfüllt) einen Präfix [0..k] besitzt so, dass alle unendlichen Erweiterungen dieses Präfixes verletzen Sicherheitsformel:p (p ist Vergangenheitsformel) verletzt p es existiert Postition k0 so, dass
(, k) p offensichtlich, für jede Erweiterung ’ von [0..k] gilt dann
(’, k) p, womit (’, k) not p gilt in der anderen Richtung: es kann gezeigt werden, dass die
oben gegebene Charakterisierung äquivalent einer kanonischen Sicherheitsformel p ist.
Entwurf von Telekommunikationssystemen - 41 - tele
Sicherheit und Lebendigkeit
Sicherheits- und Lebendigkeitsformeln Lebendigkeit
ist eine Lebendigkeitsformel gdw. wenn jede endliche Sequenz s..s zu einer unendlichen Sequenz erweitert werden kann, die erfüllt
p ist nicht die allgemein akzeptierte Definition
Entwurf von Telekommunikationssystemen - 42 - tele
Sicherheit und Lebendigkeit
Syntaktische Charakterisierung p ist eine Vergangenheitsformel, falls es keine temporalen
Zukunftsoperatoren enthält. p ist eine Zukunftsformel, falls es eine Zustandsformel ist oder falls
es eine temporale Formel mit Zukunftsoperatoren ist. Eine kanonische Sicherheitsformel ist eine Formel der Form p wobei
p eine Vergangenheitsformel ist. Eine kanonische Lebendigkeitsformel ist eine Formel der Form
wobei p .. p Vergangenheisformeln sind so, dass
gültig ist und f, .., f erfüllbare Zukunftsformeln sind Beispiele
p (wahr p) (p q) ((wahr p) (wahr q))
)fp( ii
k
1i
i
k
1i
p
Entwurf von Telekommunikationssystemen - 43 - tele
Sicherheit und Lebendigkeit
Safety-Liveness Klassifikation vs. Safety-Progress Klassifikation Die Safety-Klassen nach beiden Schemen sind identisch Die Sicherheits-Lebendigkeits Klassifikation ist orthogonal zu der
Safety-Progress Klassifikation p ist eine kanonische Response Formal, es ist gleichfalls eine
Lebendigkeitseigenschaft = (pq) ist eine Response Formel, aber keine
Lebendigketisformel
in jeder k-Klasse, k {guarantee, obligation, response, persistence, reactivity} gibt es Formeln, die Lebendigkeitsformeln sind, und andere, die es nicht sind.
q p ...
keine Möglichkeit, diese Sequenz so fortzusetzen,dass sie efüllt
Entwurf von Telekommunikationssystemen - 44 - tele
Sicherheit und Lebendigkeit
Safety-Liveness Klassifikation vs. Safety-Progress Klassifikation Jede Formel der Progress-Klasse k ist äquivalent zu einer
Konjunktions l
so, dass s Sicherheits- und l Lebendikeitsformel der Klasse k ist. Beispiel
= p U q s = (p q) l = q
Entwurf von Telekommunikationssystemen - 45 - tele
Beispiele
Alternating Bit Protocol Formulierung aus [Schwarz and Melliar-Smith] Hilfsoperatoren
p LU q (p (p U q)) U q “latches-until”: falls p gilt, und falls irgenwann einmal q gilt, dann
gilt p bis q giltp LUA q p LU (p q)
“latches-until-after”: wie LU, aber p gilt mindestens so lange bis q gilt
Variablen/Propositionen– afterDq(a): die nächste Nachricht a ist zur Übertragung
bereitgestellt– S: das letzte gesendete Paket– Si: der letzte erhaltenen Wert eines Bestätigungspaketes– corrupted(): fehlerhafte Übertragung eines Paketes– empty(): Zustand einer Warteschlange– atTs: bereit, ein weiteres Paket zu übertragen
Entwurf von Telekommunikationssystemen - 46 - tele
Beispiele
Alternating Bit Protocol "Sicherheits"anforderungen des Sendeprozesses
– R1. Aufeinanderfolgende Nachrichten werden in Paketen mit alternierenden Sequenznummern übertragen
– R2. Die Sequenz unterschiedlicher Packete, die dem Medium zur Übertragung übergeben wurde, muss identisch zu der Sequenz der empfangenen Nachrichten sein
– R3. Nachdem die Übertragung einer neuen Nachricht initiert wurde darf, bis die erste nicht verfälschte Bestätigung mit dieser Sequenznummer eingetroffen ist, nur diese Nachricht erneut übertragen werden
A1. (afterDq(a) S=<m,v>) (S=<m,v> U S=<a,v’>)A2. S = p [S = q p LUA afterDq]
[S = q p LUA (corrupted(Si) Si = q))]
Entwurf von Telekommunikationssystemen - 47 - tele
Beispiele
Alternating Bit Protocol "Lebendigkeits"anforderungen des Empfangsprozesses
– R4. Falls die Übertragung einer Nachricht initiert wurde, muss dieses Paket zumindest solange wiederholt übertragen werden, bis eine postitive Bestätigung empfangen und bemerkt worden ist
– R5. Falls wiederholte Bestätigungen für das letzte übertragene Paket unendlich häufig wiederholt erhalten werden, dann werden sie auch irgendwann bemerkt
– R6. Eine nicht korrumpierte Bestätigung, die bemerkt wurde, führt irgendwann zur Übertragung der nächsten Nachricht in der Folge der zu übertragenden Nachrichten, sofern es weitere Nachrichten gibt
A3. ((corrupted(Si) Si = S = p)) ( empty(InQ) (S p atTs))
A4. ((S = p) (S = q p)) ((S = q p atTs) U (corrupted(Si) Si = q p))
A5. ( atTs) U empty(InQ)
Entwurf von Telekommunikationssystemen - 48 - tele
Spezifikationsmuster
Ziel: Definition von Spezifikationsmustern in Termporaler Logik Speziell: Erfassung von zeitlichen Kontexten und dem
Aufeinanderfolgen von Ereignissen/Zuständen Entlastung des Spezifizierenden von der Kenntnis der konkreten
syntaktischen Formulierung einer temporalen Bedingung in LTL Beispiel:
„Between process A updating a value and process B reading the cache, the value must be flushed from A’s cache”
übersetzt sich in die folgende Formel((UpdateA ReadB) (ReadBU FlushA))
Mögliche Generalisierung Web-Site
http://www.cis.ksu.edu/santos/spec-patterns/index.html
Entwurf von Telekommunikationssystemen - 49 - tele
Spezifikationsmuster
In den Spezifikationsmustern benutzte Scopes
Entwurf von Telekommunikationssystemen - 50 - tele
Spezifikationsmuster
Occurrence Absence: Ein Zustand/Ereigniss tritt in einem Scope nicht ein Existence: Ein Zustand/Ereigniss tritt in einem Scope nicht ein Bounded Existence: Ein Zustand tritt in einem Scope k-fach auf Universality: Ein Zustand gilt in dem gesamten Scope
Order Precedence: Einem Zustand / Ereignis P muss in einem Scope
immer ein Zustand/Ereignis Q vorausgehen Response: Ein Zustand / Ereignis P muss in einem Scope immer von
einem Zustand/Ereignis Q gefolgt werden
Entwurf von Telekommunikationssystemen - 51 - tele
Spezifikationsmuster Occurrence
Absence: Ein Zustand/Ereigniss tritt in einem Scope nicht ein– Intent: To describe a portion of a system's execution that is free of certain events or states. Also known as Never. – P ist falsch:
– Beispiel: No work will be scheduled before execution.(<>call_Execute) -> ((!call_doWork) U call_Execute)
Entwurf von Telekommunikationssystemen - 52 - tele
Spezifikationsmuster Occurrence
Universality: Ein Zustand gilt in dem gesamten Scope Intent: To describe a portion of a system's execution which contains
only states that have a desired property. Also known as Henceforth and Always.
Entwurf von Telekommunikationssystemen - 53 - tele
Spezifikationsmuster Order
Precedence: Einem Zustand / Ereignis P muss in einem Scope immer ein Zustand/Ereignis Q vorausgehen
Intent: To describe relationships between a pair of events/states where the occurrence of the first is a necessary pre-condition for an occurrence of the second. We say that an occurrence of the second is enabled by an occurrence of the first.
S precedes P:
Beispiel: The computation will not terminate before the ActivePool task accepts "Complete".
((! return_Execute ) U ( return_pool.Complete || [] (!return_Execute)))
Entwurf von Telekommunikationssystemen - 54 - tele
Spezifikationsmuster Order
Response: Ein Zustand / Ereignis P muss in einem Scope immer von einem Zustand/Ereignis Q gefolgt werden Intent: To describe cause-effect relationships between a pair of events/states. An occurrence of the first, the cause, must be followed by an occurrence of the second, the
effect. Also known as Follows and Leads-to. S responds to P:
Beispiel: [](OpenNetworkConnection -> [](NetworkError -> <>ErrorMessage))
Entwurf von Telekommunikationssystemen - 55 - tele
Spezifikationsmuster Compound/Precedence/Chain
This is a scalable pattern. We describe the 1 cause - 2 effect version here. To describe a relationship between an event/state P and a sequence of events/states (S, T) in which the occurrence of S followed by T within the scope must be preceded by an occurrence of the the sequence P within the same scope.
S, T precedes P
Entwurf von Telekommunikationssystemen - 56 - tele
Bibliographische Referenzen
[Hughes and Cresswell] G. Huges and M. Cresswell, An Introduction to Modal Logic, Methuen, 1968
[Huth and Ryan] M. Huth and M. Ryan, Logic in Computer Science - Modelling and reasoning about systems, Cambridge University Press, 2000
[Manna and Pnueli 92] Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems - Specifications, Springer Verlag, 1992
[Schwarz and Melliar-Smith] R. Schwarz and M. Melliar-Smith, From State Machines to Temporal Logic: Specification Methods for Protocol Standards, IEEE Transactions on Communications, 30(12), S. 2486 - 2496, Dezember 1982.