1

Computergestützte Verifikation

04.6.2002

2

Teil II

Infinite State Systems

3

Prinzipskizze

Inf. StateModell

Formel

ABSTRAKTION Fin. StateModell

Fin. StateModel Checker

+

Gegenbeispiel

-

Analyse

Abstraktions-verfeinerung

-

Infinite State Model Checker

4

weiterer Verlauf:

5. Verifikation von Real-Time Systemen

6. Abstraktion

7. Abstraktionsverfeinerung

8. – k. Verifikation spezieller Systemklassen

Software, hybride Systeme, Security-Protokolle, Algorithmen, .....

5

5. Real Time Systeme

5.1 Timed Automata

5.2 TCTL

5.3 Abstraktion durch Regionen

5.4 Abstraktion durch Zonen

6

5.1 Timed Automata

System mit diskreten Zustandsvariablen + Uhren

Uhren haben nichtnegative reelle Werte

System hat diskrete Zustandsübergänge + Zeitverlauf

Uhren kann man auf 0 zurücksetzen oder ablesen,sie laufen alle synchron

Ablesen = diskrete Übergänge werden von Uhrenstellung beeinflußt

7

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

8

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

9

Pfade in Timed Automata

Problem: Zeitkonvergente Pfade “Zeno-Verhalten”

d1 d2 d3 d4 ....

1/2 1/4 1/8 1/16

Def: Nur die zeitdivergenten Pfade bilden die Semantik von Timed Automata

(Annahme analog zu Fairness)

10

5.2 TCTL

X-Operator wird gestrichen

D – Menge von “Formeluhren”

Constraints über D werden atomare Aussagen

c in

Beispiel: c in EF (c 5 ) = “Es ist möglich, daß in spätestens 5 s ab jetzt gilt” = EF 5

11

5.3 Regionen

Ziel: Ausnutzen, daß beim Ablesen nur mit ganzzahligen Werten verglichen wird

aber Vorsicht! Einfache Diskretisierung der Zeitachse tut’s nicht:

c1

c2

c1=1

c2<1k:= k + 1

k := k - 1

EG k < 2

gilt in keiner diskreten Zeitachse

gilt in reeller Zeitachse:

0 0.9 0.99 0.999 0.9999

12

Regionen

Region = Menge von Uhrenstellungen, die für alle Constraintsdie gleichen Werte liefern Äquivalenzrelation

ci k ci - cj k

Wann genau sind zwei Uhrenstellungen v,v’ äquivalent?

1. ganzzahlige Anteile aller Uhren gleich, oder größer als größte in Automat und Formel erwähnte Konstante2. v(c) ganzzahlig gdw. v’(c) ganzzahlig3. frac(v(c1)) < frac(v(c2)) gdw. frac(v’(c1)) < frac(v’(c2))

13

geometrische Veranschaulichung

c2

c10

1

2

1 2 3

14

Datenstruktur für Regionenganzzahlige Teile + {0, c3, c7} < {c25,c13} < ...< {c54,c8,c9,c10}

c2

c1

{0,c1}<{c2}

{0,c2}<{c1}{0,c1,c2}

{0}<{c1}<{c2}

{0}<{c2}<{c1}

{0}<{c1,c2}

15

RegionengraphZustand = [diskreter Zustand , Uhrenregion]

a) diskreter Übergang: Constraintauswertung lt. irgendeinem Element der Region, Reset liefert neue Region:

allgemein: {0,c3,c17}<{c2,c9,c54}<...< {c18,c6,c7,c8}

16

Regionengraphb) Zeitverlauf

{0} < ......... < {c2,c42,c200} {0,c2,c42,200} < ........{0,c2,c42,c200} < ....... {0} < {c2,c42,c200} < .......

17

Eigenschaften des Regionengraphs

Satz: Wenn [d,v] [d1,v1] und v’ in selber Region wie v,so ex. v1’: [d,v’] [d1,v1’] und v1’ in selber Region wie v1

(Gleiche Situation wie bei Symmetrie!)

Ein Timed Automaton erfüllt eine TCTL-Eigenschaft gdw.sein Regionengraph die zugehörige CTL-Eigenschaft erfüllt

18

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

19

Ü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

20

Ü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.)

21

Übung 3

Formuliere in TCTL die Eigenschaft:

“Auf jedem Pfad gelten a und b von jetzt an mindestens 6Zeiteinheiten lang gemeinsam, und b gilt noch 3 Zeiteinheitenlang ab dem Moment, wo a das erste Mal verletzt ist.”