1

Computergestützte Verifikation

07.6.2002

2

Übung 1

Konstruiere den Regionengraph für folgendes System (Anfang: k = 0) !Identifiziere in diesem Graph einen Pfad, der EG k 1 bezeugt!

k=0 k=1 k=2c2:=0

c1 1c2 < 1

c1 1c2 < 1

c1 1c2 < 1

c1 = 1c1:=0

c1 = 1c1:=0

c2:=0

3

Übung 2

Wie groß ist die exakte Zahl von Regionen mit Uhrenstellungen, deren ganzzahligerTeil gleich Null ist, in einem System mit genau 3 Uhren?

(Hilfe: Bei zwei Uhren wäre die Antwort 6.)

4

5. Real Time Systeme

5.1 Timed Automata

5.2 TCTL

5.3 Abstraktion durch Regionen

5.4 Abstraktion durch Zonen

5

Timed Automata

aus ein hell kaputtklickklick

klickklick

Uhren c1, c2 Uhrenmenge C

lineare Constraints: ci k oder ci - cj k (k in Nat, in {=,<,>,,,} können boolesch verknüpft sein)

c1>3c1 3 c2>10000

Invarianten (gleiche Syntax)

c2 20000

Resets = Uhren, die auf 0 gesetzt werden

c1 c2

6

Semantik von Timed Automata= “richtiges” Transitionssystem

Zustand = [d,v] d – diskreter Zustand v: C R+

Zustandsübergänge:

a) diskreter Übergang [d,v] [d’,v’] dd’ im Automat, v erfüllt Constraint an dd’, 0, falls c in Resetmenge von dd’ v’(c) = v(c), sonst v’ erfüllt Invariante in d’

b) Zeitverlauf [d,v] [d,v’] es gibt ein t 0: v’(c) = v(c) + t für alle c Jedes v+t’ (0 < t’ t) erfüllt Invariante in d

7

Regionenc2

c10

1

2

1 2 3

8

Problem des Regionengraphs

Es gibt viele Regionen:

Sei #C = n und K max. Zeitkonstante in Formel und Automat.

#Reg: O( n! x 2n-1 x Kn)

symbolisches Model Checking könnte helfen, boolescheKodierung der Regionendatenstruktur (und der Übergänge)vorausgesetzt.

wenig Erfahrung dazu, weil die meistenTools Zonen verwenden

9

Beispiel

A Bc11 c2<1 c1=1 a c2

c2>0 b c1

A,c1=0, c2=0,{0,c1,c2}

c2

c10

10

Beispiel

A Bc11 c2<1 c1=1 a c2

c2>0 b c1

A,c1=0, c2=0,{0,c1,c2} A,c1=0, c2=0,{0},{c1,c2}

c2

c10

1

1

11

Beispiel

A Bc11 c2<1 c1=1 a c2

c2>0 b c1

A,c1=0, c2=0,{0,c1,c2} A,c1=0, c2=0,{0},{c1,c2}

A,c1=1, c2=1,{0,c1,c2}

c2

c10

1

1

12

Beispiel

A Bc11 c2<1 c1=1 a c2

c2>0 b c1

A,c1=0, c2=0,{0,c1,c2} A,c1=0, c2=0,{0},{c1,c2}

A,c1=1, c2=1,{0,c1,c2}B,c1=1, c2=0,{0,c1,c2}

c2

c10

1

1

a

13

Beispiel

A Bc11 c2<1 c1=1 a c2

c2>0 b c1

A,c1=0, c2=0,{0,c1,c2} A,c1=0, c2=0,{0},{c1,c2}

A,c1=1, c2=1,{0,c1,c2}B,c1=1, c2=0,{0,c1,c2}

B,c1=1, c2=0,{0},{c1,c2}

c2

c1

0

1

1

a

2

14

Beispiel

A Bc11 c2<1 c1=1 a c2

c2>0 b c1

A,c1=0, c2=0,{0,c1,c2} A,c1=0, c2=0,{0},{c1,c2}

A,c1=1, c2=1,{0,c1,c2}B,c1=1, c2=0,{0,c1,c2}

B,c1=1, c2=0,{0},{c1,c2}

A,c1=0, c2=0,{0,c1},{c2}

c2

c10

1

1

b

a

15

Beispiel

A Bc11 c2<1 c1=1 a c2

c2>0 b c1

A,c1=0, c2=0,{0,c1,c2} A,c1=0, c2=0,{0},{c1,c2}

A,c1=1, c2=1,{0,c1,c2}B,c1=1, c2=0,{0,c1,c2}

B,c1=1, c2=0,{0},{c1,c2}

A,c1=0, c2=0,{0,c1},{c2}

A,c1=0, c2=0,{0},{c1},{c2}

c2

c10

1

1

b

a

16

Beispiel

A Bc11 c2<1 c1=1 a c2

c2>0 b c1

A,c1=0, c2=0,{0,c1,c2} A,c1=0, c2=0,{0},{c1,c2}

A,c1=1, c2=1,{0,c1,c2}B,c1=1, c2=0,{0,c1,c2}

B,c1=1, c2=0,{0},{c1,c2}

A,c1=0, c2=0,{0,c1},{c2}

A,c1=0, c2=0,{0},{c1},{c2} A,c1=0, c2=1,{0,c2},{c1}

c2

c10

1

1

b

a

17

Beispiel

A Bc11 c2<1 c1=1 a c2

c2>0 b c1

A,c1=0, c2=0,{0,c1,c2} A,c1=0, c2=0,{0},{c1,c2}

A,c1=1, c2=1,{0,c1,c2}B,c1=1, c2=0,{0,c1,c2}

B,c1=1, c2=0,{0},{c1,c2}

A,c1=0, c2=0,{0,c1},{c2}

A,c1=0, c2=0,{0},{c1},{c2} A,c1=0, c2=1,{0,c2},{c1}

A,c1=0, c2=1,{0},{c2},{c1}

c2

c11

2

1

b

a

0

18

Beispiel

A Bc11 c2<1 c1=1 a c2

c2>0 b c1

A,c1=0, c2=0,{0,c1,c2} A,c1=0, c2=0,{0},{c1,c2}

A,c1=1, c2=1,{0,c1,c2}B,c1=1, c2=0,{0,c1,c2}

B,c1=1, c2=0,{0},{c1,c2}

A,c1=0, c2=0,{0,c1},{c2}

A,c1=0, c2=0,{0},{c1},{c2} A,c1=0, c2=1,{0,c2},{c1}

A,c1=0, c2=1,{0},{c2},{c1}

A,c1=1, c2=1,{0,c1},{c2}

c2

c11

2

1

b

a

0

19

Beispiel

A Bc11 c2<1 c1=1 a c2

c2>0 b c1

A,c1=0, c2=0,{0,c1,c2} A,c1=0, c2=0,{0},{c1,c2}

A,c1=1, c2=1,{0,c1,c2}B,c1=1, c2=0,{0,c1,c2}

B,c1=1, c2=0,{0},{c1,c2}

A,c1=0, c2=0,{0,c1},{c2}

A,c1=0, c2=0,{0},{c1},{c2} A,c1=0, c2=1,{0,c2},{c1}

A,c1=0, c2=1,{0},{c2},{c1}

A,c1=1, c2=1,{0,c1},{c2}

c2

c10

1

1

b

a

a

20

5.4 Abstraktion durch Zonen

Problem des Regionengraphs: Zu viele Regionen neue Idee: größere Einheiten

Zone = Menge von Uhrenstellungen, die durch eine Konjunktionvon Uhrenconstraints (ci k oder ci - cj k, in {=,<,>,,,}) beschreibbar ist

Vereinfachende Annahmen: Constraints und Invarianten imTimed Automaton seien nur per Konjunktion verknüpft sind ihreserseits Zonen

21

geometrische Veranschaulichung

0 c1

c2

c1>2

c2 – c1 0

c1 – c2 < 4

c2 > 1

c2 3

c1 4

22

Zonen

Zonen sind konvexe Polyeder

Ränder können, müssen aber nicht dazugehören ( </)

manche Seiten können bis ins Unendliche offen sein

Jede Region ist eine Zone

Jede Zone ist Vereinigung von Regionen

manchmal in der Literatur: Zone = Region, Region = atomare Region

23

Operationen auf Zonen: DurchschnittDer Durchschnitt zweier Zonen ist eine Zone

Benutzung: Bestimmung der Menge aller Uhrenstellungenin einer Zone die ein Constraint/ eine Invariante erfüllen

0

c2

24

Operationen auf Zonen: ProjektionWenn Z eine Zone ist, so auch{[x1,....,xi-1,0,xi+1,...,xn] | [x1,....,xi,....,xn] Z}

0 c1

Benutzung: Uhr auf 0 setzen

25

Operationen auf Zonen: ÖffnungWenn Z Zone ist, so auch{ [x1+t,....,xi+t,....,xn+t] | [x1,...,xn] Z, t R+}

0

Benutzung: Zeitverlauf

26

Nachfolgezone

geg: [d,Z] Nachfolger: [d’,Z’] so, daß

-Zu jedem v’ in Z’ ex. ein v in Z mit - [d,v] [d’,v1] (diskreter Übergang) - [d’,v1] [d’,v’] (Zeitverlauf)

Lösung:1. Schneide z mit Constraint am Übergang2. Projiziere für alle Uhren in der Resetmenge3. Schneide mit Invariante am neuen diskreten Zustand4. falls entstandene Zone nicht leer, Öffne5. Schneide mit Invariante am neuen diskreten Zustand

Startzone: 0-Zone +Öffnung + Schnitt mit Invariante desAnfangszustandes

27

Beispiel

A Bc11 c2<1 c1=1 a c2

c2>0 b c1

0

c2

s0: [A, Z1]

s1: [B,Z2]

s2: [A,Z3]

Zonengraph:Von [d,Z1],[d,Z2] mit Z1Z2,behalte nur [d,Z2]

28

Zonengraph: bewahrte Eigenschaften

Für jede Eigenschaft aus ACTL* gilt:

Wenn im Zonengraph gilt, so gilt im originalen Transitionssystem

ACTL*: Nur A als Pfadquantor keine Negation (bzw.: Negation nur auf elementaren Zustandseigenschaften)

ACTL*: “universelle Eigenschaften” >90% der Spezifikationen in der Praxis sind in ACTL*

Die im Zonengraph repräsentierten Zustände sind genau dieerreichbaren

29

Beziehung zwischen den Logiken

CTL*

CTL LTL

ACTL*

30

Implementation von Zonen

bisher: Zone = Konjunktion von Constraints

Problem: Eine Zone hat viele Darstellungen

Lösung: Normalform

=- für jedes c1,c2 C{0} genau ein Constraint der Form c1 – c2 k oder c1 – c2 < k ( K aus Int {} )

-jeweils das “engstmögliche” Constraint (kleinstmögliches k, das engstmögliche Relationszeichen)

Normalform ist eindeutig!

31

geometrische Veranschaulichung

0 c1

c2

0 - c1< -2

c2 – c1 0

c1 – c2 < 4

0 - c2 < -1

c2 - 0 3

c1 – 0 4

c1 – c2 < 3

32

Berechnung engerer Constraints

c1

c1 – c2 < 4

0 - c2 < -1c1 – 0 4

c1 – c2 < 3

c1 – 0 4+ 0 - c2 < -1 c1 – c2 < 3

33

Normalisierung

Algorithmus: 1. Wandle Constraints ci k in Constraints ci – 0 </ k und/oder 0 – ci </ -k um2. Für jedes ci,cj aus C {0} behalte das engste Constraint bzw. füge ci – cj < ein3. Wiederhole, bis nix Neues: Für jedes ci – cj k1 , cj – ck ’ k2, füge ci – ck ” k1+k2 ein, falls es enger ist als das vorhandene Constraint für ci – ck; ” = ‘’, falls , ’ = ‘’, sonst ‘<‘

Algorithmus führt zu Normalform

34

Shortest Path Closure= Graphalgorithmus für Normalisierung

ci

cj

ck

k1 k2

k

ci - cj

min(k,k1+k2)

Algorithmus von Floyd & WarshallO(n3)

geg: Graph G mit “Kosten” für jede Kanteges: Graph G’, wo an jeder Kante [a,b] die Kosten des billigstenWeges von a nach b in G stehen

anzuwenden auf difference bound matrix:

c1

c3

0

c2

35

Implementation von Operationen:Durchschnitt

geg: Z1,Z2 als difference bound matrix in Normalform

ges: Z1Z2 als Difference bound matrix in Normalform

Lösung: Nimm das jeweils engere Constraint ausZ1 oder Z2, dann nachnormalisieren

36

Implementation von Operationen:Projektion auf c*

geg.: Z in Normalform ges: Projektion Z’ auf c*

ci – 0 k ci – c* (egal) in Z

ci – 0 kci – c* k in Z’

0 – ci k c* – ci (egal) in Z

0 – ci kc* – ci k in Z’

restliche Constraints unverändert

keine Nachnormalisierung notwendig

0 – c* (egal) c* - 0 (egal) in Z

0 – c* 0c* - 0 0 in Z’

Lösung: “alles, was vorher für 0 stimmte, stimmt jetzt auch für c*”

37

Implementation von Operationen:Öffnung

geg: Z ges: Z’

Lösung:

1. Constraints c – c’ für c,c’ 0 bleiben unverändert2. Constraints 0 – c bleiben unverändert3. Aus Constraints c – 0 k wird c – 0 <

keine Nachnormalisierung notwendig

38

Das Beispiel noch mal ordentlichA Bc11 c2<1

c1=1 a c2

c2>0 b c1

0

c2s0: [A, Z1]

s1: [B,Z2]

s2: [A,Z3]

0 c1 c2 0 0 0 0c1 0 0 0c2 0 0 0

0 c1 c2 0 0 0 0c1 < 0 0c2 < 0 0

0 c1 c2 0 0 0 0c1 1 0 0c2 1 0 0

Ö

0 c1 c2 0 0 0 0c1 1 0 1c2 << 0

=

39

Das Beispiel noch mal ordentlichA Bc11 c2<1

c1=1 a c2

c2>0 b c1

0

c2s0: [A, Z1]

s1: [B,Z2]

s2: [A,Z3]

0 c1 c2 0 0 -1-1c1 1 0 0c2 1 0 0

0 c1 c2 0 0 0 0c1 1 0 0c2 1 0 0

0 c1 c2 0 0 -10c1 1 0 1c2 << 0

=

0 c1 c2 0 0 -10c1 1 0 1c2 0 -10

P c2 usw

40

Explizites Real-Time Model Checking

Welches Reduktionstechniken greifen?

Symmetrien: no problem

Partial Order Reduction:Problem: “Zeitverlauf” kann viele...alle Aktionen aktivierenoder deaktivieren, und ist fast immer aktiviert wenig UnabhängigkeitLösung? : “Prozeßlokale” Uhren, die sich nur für Interprozeßkommunikation synchronisieren, sonst asynchron laufen

mangelnder Erfolg der Partial Order Reduction begrenztexplizites Model Checking (... obwohl schon winzige Real-Time Systeme komplex (=fehlerhaft) sein können)

...wenn, dann mit Zonen.

41

Symbolisches Real-Time Model Checking

Regionen: kein Problem, nur Frage von Kodierung undVariablenordnung

Zonen: Problem: arithmetische Operationen, speziell Normalisierung

Lösung: Datenstruktur, die wie BDD funktioniert, aber“arithmetischer”/”zoniger” ist

Clock Difference Diagrams; CDDData Decision Diagrams; DDD Multidecision Diagrams; MDD

42

Clock Difference Diagrams

ci - cj

[0,3) [3,17] (17,)

-Nachbildung aller BDD-Operationen, plus-Projektion-Öffnung-Schnitt

aber: lange Zeit offen: Normalisierung(inzwischen wohl gelöst für DDD)

43

Übung 1

Konstruiere den Zonengraph für folgendes System (Anfang: k = 0) !Identifiziere in diesem Graph einen Pfad, der EG k 1 bezeugt!

k=0 k=1 k=2c2:=0

c1 1c2 < 1

c1 1c2 < 1

c1 1c2 < 1

c1 = 1c1:=0

c1 = 1c1:=0

c2:=0

44

Übung 2

Wie kann man zu zwei in Normalform als Difference BoundMatrix gegebenen Zonen feststellen, ob eine der beideneine Teilmenge der anderen beschreibt?

45

Übung 3

Warum kann man die Regionengraphkonstruktion nichtauf Stopwatch-Automaten anwenden?