Tele Entwurf von Telekommunikationssystemen- 197 - Ü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


Automatenmodelle und Logiken

Operationelle Anforderungsspezifikationen und architekturelle Designspezifikationen für reaktive Systeme werden häufig in automatenbasierten Formalismen verfasst SDL

– ITU-T Recommendation Z.100– CEFSM-Modell mit beliebigen Datenbereichen und

unbeschränkten Kommunikationskanälen Real-Time Object-Oriented Modeling (ROOM)

– Verhalten basiert auf HCEFSMs UML for Real-Time (UML RT)

– syntaktische Variante von ROOM

Abstrakte Anforderungen können gut durch Automaten oder temporallogische Formeln dargestellt werden


Anforderungsvalidation

Anforderungs-analyse und Vereinbarung

Anforderungs-dokumentation

und SpezifikationValidation

Kunden- oder Be-

nutzeranforderungen

(abstrakt)

Anforderungs-

ermittlung

Vereinbarte undValidierte

Anforderungen

AutomatenmodellM

Automaten- oderLogikspezifikation

L

M L“model checking”



M

(Operationelles

Anforderungsmodell)

L(abstrakte

Anforderungen)

1

0



Weitere Anwendungsbeispiele Implementiert ein Design die Anforderungsspezifikation? Korrektheit einer Implementierung: erfüllt eine Implementierung auf

beliebiger Stufe die Anforderungen? Code-Verifikation: erfüllt der Quellcode die Anforderungen?

System design

Requirements

Design

Implementation

Integration

Maintenance


Prinzip des Model Checking

Beispiel: Mutual Exclusion (Gegenseitiger Ausschluss) zwei Prozesse, i = 1, 2 globaler Zustandsraum, Zustände S1, .., S9 Zustandspropositionen

– n: Prozess i ist nicht im kritischen Abschnitt– t: Prozess i versucht, in den kritischen Abschnitt zu gelangen– c: Prozess i befindet sich in dem kritischen Abschnitt

Spontane Transitionen zwischen Zuständen Interleaving Semantik für Nebenläufigkeit



Gegenseitiger Ausschluss

S0n1n2

S4t1t2

S3c1n2

S1t1n2

S7c1t2

S6n1c2

S5t1t2

S2n1t2

S8t1c2



Sicherheitsanforderungen Es befinden sich nie zwei Prozesse gleichzeitig in dem kritischen

Abschnitt Formalisierung

(c1c2)

S0n1n2

S4t1t2

S3c1n2

S1t1n2

S7c1t2

S6n1c2

S5t1t2

S2n1t2

S8t1c2



Sicherheitsanforderungen Validationsprinzip: besuche jeden Zustand und überprüfe, ob die

Eigenschaft in jedem Zustand erfüllt ist Wenn alle Zustände die Eigenschaft erfüllen, dann kann man keinen Präfix

so fortsetzen, dass er die resultierende Folge die Eigenschaft verletzt

S0n1n2

S4t1t2

S3c1n2

S1t1n2

S7c1t2

S6n1c2

S5t1t2

S2n1t2

S8t1c2



Lebendigkeitsanforderung In jedem Zustand gilt, dass entweder Prozess 1 oder Prozess 2 immer

irgendwann einmal in den kritischen Bereich gelangen werden Formalisierung

(c1 c2)

S0n1n2

S4t1t2

S3c1n2

S1t1n2

S7c1t2

S6n1c2

S5t1t2

S2n1t2

S8t1c2



Lebendigkeitsanforderung Validationsprinzip

– Besuche jeden Zustand und überprüfe, ob ein Zyklus in dem Graphen gefunden werden kann, der die Bedingung verletzt

– analog: nicht alle unendlichen Verlängerungen aller endlichen Präfixe erfüllen die Eigenschaft

S0n1n2

S4t1t2

S3c1n2

S1t1n2

S7c1t2

S6n1c2

S5t1t2

S2n1t2

S8t1c2



Response Wenn ein Prozess einmal versucht, in den kritischen Bereich zu

gelangen, dann wird er auch irgendwann den kritischen Bereich erreichen

Formalisierung (t1 c1) (t2 c2)

S0n1n2

S4t1t2

S3c1n2

S1t1n2

S7c1t2

S6n1c2

S5t1t2

S2n1t2

S8t1c2



Suchstrategien Tiefensuche (depth-first-search) mehrfach

Allgemeine Strategien? Model checking für beliebige Formeln der temporalen Logik

S0n1n2

S4t1t2

S3c1n2

S1t1n2

S7c1t2

S6n1c2

S5t1t2

S2n1t2

S8t1c2


Temporale Logik und Automaten Es gibt eine enge Verbindung zwischen Büchi-Automaten und

temporaler Logik LTL entspricht Zähler-freien Büchi-Automaten und *-freien -regulären

Ausdrücken Büchi-Automaten sind echt ausdrucksstärker als LTL-Formeln Ausdruckfähigkeit temporaler Logik im Vergleich zu Automaten nach [Wolper]:

LTL

ETL

Zähler-freie Büchi-Automaten

*-freie -reguläre

Sprachen

NichtZähler-freie Büchi-

Automaten

-reguläre Sprachen


Beispiel einer Eigenschaft, die mit allgem. Büchi-Automaten, aber nicht mit LTL ausgedrückt werden kann

even(p): Proposition p ist wahr in jedem geradezahlig numerierten Zustand der Ausführungsfolge

Büchi:

-reg: (p) LTL:

: p (p p) (p p)kann diese Eigenschaft nicht vollständig charakterisierensei =dann gilt even(p) und

Schluss: – mit LTL können Eigenschaften, die wiederholtes Zählen bis zu

einer Konstanten n erfordern, nicht ausgedrückt werden.– Büchi Automaten können zählen modulo eines festen n– für jede LTL-Formel gibt es einen gleich ausdrucksstarken Büchi-

Automaten– Für Beweise siehe [Wolper]

Temporale Logik und Automaten

p p p …

p S0S1



Intuitiv: LTL-Formeln und äquivalente Automaten

(c1 c2) S0 S1

(c1 c2)

(c1 c2)

wahr

(c1 c2) S0 S1

(c1 c2) c1 c2

(c1 c2)

c1 c2




(p q)

(p q)

(p q)

q

S0 S1

wahr

p q

S0 S1

p (pq)

q

pqq




(p (r W q))

(p (r U q))

S0 S1

p (pq)

q

p r q

r q(p (r U q)) ?

q r

S0 S1

wahr

S2

p r q

p r q r q

wahr



Vorgehen Sei A eine Systemspezifikation, gegeben als ein Büchi Automat Sei S eine Spezifikation, gegeben als ein Büchi Automat Seien L(A) und L(S) die von A bzw S akzeptierten Sprachen A erfüllt die Spezifikation S, falls L(A) L(S)

Anwendungs auf Anforderungsvalidation

S

(Operationelles

Anforderungsmodell)

A(abstrakte

Anforderungen)

1

0

L(A) L(S)



Komplementierung von Büchi-Automaten Sei - L(S) = comp(L(S)) dann L(A) L(S) L(A) comp((L(S)) Büchi-Automaten sind abgeschlossen unter Komplementbildung und

Durchschnitt, d.h.,– es gibt einen B.A., der comp((L(S)) repräsentiert, und– es gibt einen B.A., der L(A) comp((L(S)) repräsentiert

Implementierungsvarianten– direkte Komplementierung von S: Komplementierung von B.A. ist

eine nicht-triviale Operation (siehe [Sistla, Vardi and Wolper]– direkte Spezifikation von comp(S): Wird teilweise in Model

Checkern vorgesehen (never-claims in Promela/SPIN)– spezifiziere LTL-Formel , benutze Negation , übersetze in

einen äquivalenten B.A.



Existenz eines Gegenbeispiels L(A) comp((L(S)) = A erfüllt S L(A) comp((L(S)) = C C ist Gegenbeispiel für die

Nichterfüllung von S durch A– es kann gezeigt werden, dass jedes Wort in C in der Form uv

repräsentiert werden kann, wobei u und v endliche Zustands- oder Ereignisfolgen sind


Prinzip des Model Checking Konstruktion eines Schnittmengen-Büchi-Automaten

SeienM = (Q, q0, A, , F) undM = (Q, q0, A, , F)

zwei Büchi-Automaten. Der L(M) L(M) akzeptierende Automat kann definiert werden als

M M = ( Q x Q x {0, 1, 2}, (q0, q0, 0), A, , Q x Q x {2} )so, dass (<r,q,x>, a, <r, q, y>) gdw alle folgenden

Bedingungen gelten:– (r, a, r) und (q, a, q) (die Transitionen des

Schnittmengen-B.A. stimmen mit den Transitionen der einzelnen B.A. überein)

– die dritte Komponente der Zustandspaare ergibt sich wie folgt: falls x=0 und r F, dann y = 1 falls x=1 und q F, dann y = 2 falls x=2, dann y = 0 andernfalls, y=x


Prinzip des Model Checking Beispiel (aus [Clarke, Grumberg and Peled])

r

a b

a

b

r q

b a

b

a

q

a b

a ba

b b

b a

a

r,q,0

r,q,1 r,q,0

r,q,2 r,q,0

M M

M M


Prinzip des Model Checking Konstruktion eines Schnittmengen-Büchi-Automaten

Letzte Komponente stellt sicher, dass Zustände sowohl von M als auch von M in einem akzeptierenden Zyklus unendlich häufig vorkommen

Definition von F = F x F wäre nicht ausreichend, da dann Zyklen akzeptiert würden, die nur durch den Akzeptierungszustand eines der B.A. unendlich zirkulieren würden

Dritte Komponente:– von 0 auf 1, wenn ein akzeptierender Zustand des ersten

Automaten erreicht wird, – von 1 auf 2 (Akzeptierungszustand), wenn ein akzeptierender

Zustand des zweiten Automaten erreicht wird,– von 2 im nächsten Zustand auf 0



Leerheitsüberprüfung für Büchi-Automaten Sei M = (Q, q0, A, , F) ein Büchi-Automat Sei ein Lauf auf so dass von M akzeptiert wird enthält unendlich viele akzeptierende Zustände aus F Da Q endlich ist, gibt es einen Suffix ’ von so dass jeder Zustand

in ’ unendlich häufig vorkommt Jeder Zustand in ’ ist von jedem anderen Zustand in ’ erreichbar,

d.h., die Zustände in ’ sind teil einer starkt verbundenen Komponente (strongly connected component - Clique?) von M, die von q0 erreichbar ist

D.h., die Frage L(M) = ist äquivalent der Auffindung einer stark verbundenen Komponente im Zustandsgraphen von M

-> Tarjan’s Tiefensuche (depth first search, DFS), lineare Zeit– Ableitung Gegenbeispiel

Die Mitglieder jeder gefundenen Komponente bilden den unendlich wiederholten Suffix

Der Erreichbarkeitspfad der Komponente von q0 bildet Präfix Effizientere Lösung für praktische Probleme: zweifacher DFS



Zweifacher DFS (nach [Clarke, Grumberg and Peled])

procedure emptiness

dfs(q);terminate(false)

end procedure

procedure dfs1(q)

local q’;

hash(q);

for all successors q’ of q do

if q’ not in hashtable

then dfs1(q’)

end if;

if q F then dfs2(q)end if;

end do;

end procedure

procedure dfs2(q)

local q’;

flaq(q);

for all successors q’ of q do

if q’ on dfs1-stack

then terminate(true)

else if q’ not flagged

then dfs2(q’)

end if;

end do;

end procedure



Zweifacher DFS (nach [Clarke, Grumberg and Peled]) Ableitung des Gegenbeispiels bei terminate(true)

– dfs2(s)– s wird von dfs2 auf dfs1-stack gefunden– Konstruktion Gegenbeispiel:

q0 ss


Prinzip des Model Checking Synchrones Produkt ([Holzmann 95])

Idee– Sei M ein B.A., der dem zu validierenden Transitionssystem

entspricht– Sei L ein B.A., welcher der zu validierenden Eigenschaft

entspricht Transitionen von L sind mit propositionalen Ausdrücken

markiert, die sich auf die Zustandsvariablen von M beziehen– Führe einen Matching durch zwischen den Zuständen von M und

den Transitionen von L

...

...

...

x

y

c

...

...

...

w

v

vc“match”

vons’ und

(s, s)

M L

L: s, .., s=x, s=y, .. M: s’, .., s’=v, ..



Idee– Ziel: erzeuge alle akzeptierenden Läufe von L, die auch

akzeptierende Läufe von M sind– Ein Lauf von L passt („match“) auf einen Lauf von M, falls alle

Zustände in L’s Lauf auf alle Zustände in Mäs Lauf passen– Ein akzeptierender Lauf auf L, der einem passenden Lauf auf M

entspricht, beschreibt eine Ausführungsfolge, die der durch L ausgedrückten (unerwünschten) Eigenschaft entspricht

– Absenz eine akzeptierenden Laufs von L, für den es einen passenden Lauf von M gibt, bedeutet, dass die (unerwünschte) Eigenschaft nicht gilt

...

...

...

x

y

c

...

...

...

w

v

vc“match”

vons’ und

(s, s)

M L

L: s, .., s=x, s=y, .. M: s’, .., s’=v, ..



Beispiel

at_ix

at_ix

at_ix

at_i

at_i

wahr at_i

at_iy y

Negation

(x, y) (x, y) (x, y)

(x, y) (x, y)

M

L

P



Beispiel– Jeder Lauf des Produktautomaten P entspricht einem Lauf von M genauso wie einem Lauf von L– Jeder akzeptierende Lauf von P entspricht damit einem Lauf von M und einem akzeptierenden Lauf von L, womit gezeitgt wird, dass die Schnittmenge der von beiden Automaten akzeptierten

Sprachen nicht leer ist

(x, y) (x, y) (x, y)

(x, y) (x, y)

P



Beispiel– Die von L ausgedrückte Eigenschaft hält für M, da das Synchrone

Produkt P einen akzeptierenden Zyklus enthält (zweifach DFS)– Gegebeispiel: (x, y) , (x, y), (x, y)

(x, y) (x, y) (x, y)

(x, y) (x, y)

P



Beispiel 2

at_ix

at_ix

at_ix

at_i

at_i

wahr at_i

at_iy y

Negation

(x, y) (x, y) (x, y)

(x, y) (x, y)

M

L

P

Kein Akzeptierender Lauf von P, daher (unerwünschte) Eigenschaft nicht erfüllt.


Bibliographische Referenzen [Clarke, Grumberg and Peled] E. Clarke, O. Grumberg

and D. Peled, Model Checking, MIT Press, Cambridge, 1999

[Holzmann 95] G. Holzmann, The Verification of Concurrent Systems, unpublished manuscript, AT&T Inc., 1995

[Holzmann 97] G. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, Vol. 23, No. 5, May 1997

[Sistla, Vardi and Wolper] A. Sistla, M. Vardi and P. Wolper, The complementation problem for Büchi Automata with applications to temporal logic, Theoretical Computer Science, 49: 217 - 237

[Wolper] P. Wolper, Temporal Logic can be more expressive, Information and Control, Vol. 56, S. 72-99, 1983

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

Documents

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