1

Computergestützte Verifikation

23.4.2002

2

Inhalt

System Abstraktion

Spezifikation

Simulation

Formalisierung

Model Checker

Gegenbeispiel

Modell

log. Formel

+

-

VerfeinerungFehler-beseitigung

Präzisierung

Überlauf

Kapitel 1: Systeme

Kapitel 2: Temporale Logik

3

Temporale Logik

Eigenschaften von Zuständen undderen Änderung in Systemabläufen

Erweiterung der Aussagenlogik

4

Zustandseigenschaften

“Mailbox ist leer” “bin bei Anweisung k”

“x[17] > 35” “nil dereferenziert”

k,q,nq,n

q

x,k

Annahme: s(p) mit vernachlässigbarem Aufwandberechenbar aus Repräsentation von s im Rechner

5

CTL*

CTL*

LTL CTL

nur Pfad-formeln

Nur Zust.-formeln

X, F, G, U X, F, G, U,A, E

EX, AX,EF, AF,EG, AG,E( . U . )A( . U . )

6

Progress und Fairness

p

a

bc

d

e

f

p p p

a

b

d e

F p gilt nicht !!?!?!?!

7

Lösung: Fairnessannahmen

Eine Fairnessannahme ist eine Pfadeigenschaft undBestandteil der Systembeschreibung.

Gültigkeit unter Fairness:A = für jeden Pfad, der alle Fairnessannahmen erfüllt, gilt....E = es gibt einen Pfad, der alle Fairnessannahmen erfüllt und ...

Fairness

aktionsbasiert zustandsbasiert

8

Progress (= schwache Fairness)

zustandsbasiert:Eigenschaften der Form G F ist Zustandseigenschaft)werden Progress-Annahmen genannt (oder schwacheFairnessannahmen).

Beispiele: G F pc k GF input = 0 GF input = 1

aktionsbasiert:Ein Pfad behandelt eine Aktion a schwach fair, wenn:Wenn a in von einem Zustand s an unendlich lange aktiviertist, wird a bei einem Nachfolger von s ausgeführt

informal: Komponenten bleiben nicht einfach so stehen

9

Starke Fairness

zustandsbasiert:Eigenschaften der Form (G F ) (G F ) werdenstarke Fairnessannahmen genannt.

Beispiel: ( G F ressource beantragt ) ( G F ressource erhalten)

aktionsbasiert:Ein Pfad p behandelt eine Aktion a stark fair, wenn:Wenn a in p unendlich oft enabled ist, wird a auchunendlich oft ausgeführt

informal:Wenn sich mehrere Prozesse wiederholt um geteilteRessourcen bewerben, kommt jeder mal dran

10

Fairness - Zusammenfassung

Spezifikation = Sicherheitseigenschaft + Lebendigkeitseigenschaft

Fairnessannahmen sind Lebendigkeitseigenschaften

Vorsicht! k: receive(m,Mailbox)

G F pck G F (pckMailbox=)

System = Transitionssystem + Fairnessannahmen

11

BeispieleWechselseitiger Ausschluss

S: G (pc1 “critical” pc2 “critical” )

L: G (pc = “request” F pc = “critical”)

TS: Pr i (pc: lokale Variable, sem: globale Variable) init(pc) = “idle” init(sem) = 1 g0: pc = “idle” pc = “idle” /* do something else */ g1: pc = “idle” pc = “request” g2: pc = “request” sem = 1 sem = 0, pc = “critical” g3: pc = “critical” pc = “idle”, sem = 1

F’: G F pc “critical” , (G F (pc = “request” sem = 1)) (G F pc = “critical”)

F: schwach: g3 stark: g2

12

Beispiele

F’: G F pc “critical” , (G F (pc = “request” sem = 1)) (G F pc = “critical”)

F: schwach: g3 stark: g2

(i,i,1)

(r,i,1) (i,r,1)

(r,r,1)(c,i,0) (i,c,0)

(c,r,0) (r,c,0)

g2

g1 g1’

g2’g1

g1

g1’

g1’

g3 g3’

g3’g3

g2’g2

g0,g0’

g0

g0

g0’

g0’

13

Beispiele

F’: G F pc “critical” , (G F (pc = “request” sem = 1)) (G F pc = “critical”)

F: schwach: g3 stark: g2

(i,i,1)

(r,i,1) (i,r,1)

(r,r,1)(c,i,0) (i,c,0)

(c,r,0) (r,c,0)

g2

g1 g1’

g2’g1

g1

g1’

g1’

g3 g3’

g3’g3

g2’g2

g0,g0’

g0

g0

g0’

g0’

schwach unfairbzgl. g2

14

Beispiele

F’: G F pc “critical” , (G F (pc = “request” sem = 1)) (G F pc = “critical”)

F: schwach: g3 stark: g2

(i,i,1)

(r,i,1) (i,r,1)

(r,r,1)(c,i,0) (i,c,0)

(c,r,0) (r,c,0)

g2

g1 g1’

g2’g1

g1

g1’

g1’

g3 g3’

g3’g3

g2’g2

g0,g0’

g0

g0

g0’

g0’

schwach fair, aberstark unfair bzgl.g2

15

Beispiele

F’: G F pc “critical” , (G F (pc = “request” sem = 1)) (G F pc = “critical”)

F: schwach: g3 stark: g2

(i,i,1)

(r,i,1) (i,r,1)

(r,r,1)(c,i,0) (i,c,0)

(c,r,0) (r,c,0)

g2

g1 g1’

g2’g1

g1

g1’

g1’

g3 g3’

g3’g3

g2’g2

g0,g0’

g0

g0

g0’

g0’

fair, gewollter Ablaufwäre schwach unfairbzgl. g1

16

Beispiele“Echo”: propagation of information with feedback

Prozess initiator (1) Prozesse other (n)

Kommunikationsrelation N (bidirektional, zusammenh.)Nachricht: [Empfänger, Absender, Inhalt]

initiator:g1: pc = idle c = choose, pc = activeg2: pc = active send(N(myself) x {myself} x {c}),pc = waitingg3: pc = waiting received({myself} x N(myself} x {c}) pc = ready

other:g4: pc = idle received([myself,f,c]) send(N(myself) \ {f} x {myself} x {c}), pc = pendingg5: pc = pending received(N(myself) \ {f} x {myself} x {c}) send([f,myself,c]), pc = terminated

F: schwach: g2-g5

L: G (initiator.pc = active F initiator.pc = ready)S: G (initiator.pc = ready o.c = initiator.c)

o in other

17

Wie geht es weiter?

System Abstraktion

Spezifikation

Simulation

Formalisierung

Model Checker

Gegenbeispiel

Modell

log. Formel

+

-

VerfeinerungFehler-beseitigung

Präzisierung

Überlauf

A) Finite state systems B) Infinite state systems

18

Model Checking für finite state systems

explizit: symbolisch:

explizite Konstruktion einesTransitionssystems,

das sich in bezug auf dieuntersuchte Eigenschaftäquivalent zum gegebenenverhält, aber in der Regelwesentlich kleiner ist.

Eigenschaft wird durchGraphsuche nach Zeugen/Gegenbeispielenverifiziert

Datenstruktur, die Mengen vonZuständen bzw. Pfadenbeschreibt,Operationen, die simultan dieNachfolger aller Zuständeberechnet

Eigenschaft wird durch Fixpunktoperationen auf dersymbolischen Datenstrukturberechnet

19

Model Checking für finite state systems

explizit: symbolisch:

3.1: Tiefensuche

3.2: LTL-Model Checking

3.3: CTL-Model Checking

3.5: Reduktion durch Symmetrie3.6: Partial Order Reduction

3.7: Tools

4.1: BDD-basiertes CTL-Model Checking

4.2: SAT-basiertes Model Checking

4.3: Tools

3.4: Fairness

Kapitel 3 Kapitel 4

20

Kapitel 3

3.1. Tiefensuche

Explizites Model Checking

21

Setting

Geg.: Gerichteter Graph [V,E]

Ges.: stark zusammenhängende Komponenten

v ~ v’ gdw. Es gibt einen Weg von v nach v’ und einen Weg von v’ nach v in G

~ ist Äquivalenzrelation; Klassen heißen SZK.

SZK können durch Tiefensuche ermittelt werden (Tarjan ’72)

22

Einfache Tiefensuche

Annahme: Graph [V,E] zusammenhängend von v0

VAR schwarz, grau, weiss: Knotenmengen, dfs: Nat

schwarz := grau := , weiss := V, maxdfs := 0dfs(v0);

dfs(v)v.dfs = maxdfs; maxdfs += 1;

weiss := weiss \ {v}, grau := grau {v};FOR ALL v’ ([v,v’] E) DO

IF v’ weiss THENdfs(v’)

ENDENDgrau := grau \ {v}; schwarz := schwarz {v};

Invariant: weissgrau schwarz = V, schwarz reach(grau) = V

Ende: grau =

23

Tiefensuchbaum

Tiefensuche definiert Numerierung der Knoten (dfs)und Tiefensuchbaum [V,T]:[v,v’] T gdw. dfs(v’) wird von dfs(v) aus aufgerufen

Beispiel:

v0 0

3

26

1

5

4

0

6

52

4

1

3

24

SZK und Tiefensuchbaum

0

3

26

1

5

4 Jede SZK bildet einenzusammenängenden Bereichim Tiefensuchbaum

Wurzel des Teilbaums istKnoten mit kleinster dfs.

[v,v’] in T v.dfs < v’.dfs

In jedem Teilbaum ist dieMenge der Tiefensuchnummernlückenlos

0

6

52

4

1

3

25

Klassifikation von E

0

3

26

1

5

4 [v,v’] ist Vorwärtskante, falls [v,v’] in T*\T

[v,v’] ist Rückwärtskante, falls [v’,v] in T*

[v,v’] ist Querkante, sonst

[v,v’] ist Baumkante, falls [v,v’] in T

[v,v’] in Quer v.dfs > v’.dfs

[v,v’] in Vorwärts v.dfs v’.dfs

[v,v’] in Rückwärts v.dfs > v’.dfs

[v,v’] in Rückwärts v ~ v’0

6

52

4

1

3

26

Kriterium für Startknoten von SZK

0

3

26

1

5

4v.lowlink = MIN(v’.dfs | v’ von v erreichbar über beliebig vieleBaumkanten, gefolgt von max. eineranderen Kante [v,v’] mit v ~ v’)

0

1

1

3

4

44

Satz: v ist genau dann Startknoten einerSZK wenn v.lowlink = v.dfs

0

6

52

4

1

3

0

1 1

1

6

4

4

27

Tarjans AlgorithmusVAR Tarj: Stack von Knoten, maxdfs: Nat, weiss: Knotenmengeweiss := V, maxdfs = 0; Tarj := empty stackdfs(v0);

dfs(v): v.dfs = v.lowlink = maxdfs; maxdfs += 1;push(v,Tarj);weiss := weiss \ {v}FOR ALL v’ ([v,v’] in E) DO

IF v’ in weiss THENdfs(v’)v.lowlink = MIN(v.lowlink,v’.lowlink)

ELSEIF v’ on Tarj THEN

v.lowlink = MIN(v.lowlink,v’.dfs)END

ENDENDIF v.lowlink = v.dfs THEN

REPEATv* = pop(Tarj)

UNTIL v = v*END

eine SZK

Baumkante

andere Kante

28

lowlink wird korrekt berechnet

....

ELSE

IF v’ on Tarj THEN

v.lowlink = MIN(v.lowlink,v’.dfs)

END

END

....

Fall 1: [v,v’] Vorwärtskante: also v.dfs < v’.dfs, also trägt v’ nicht zum Minimum bei

... gefolgt von einer anderen Kante [v,v’] mit v ~ v’

Fall 2: [v,v’] Rückwärtskante: also v ~ v’, v’ vor v im Stack, also v’ noch auf Tarjanstack

Fall 3: [v,v’] Querkante: ok, siehe Tafelskizze

29

Fazit Kapitel 3.1

Wir haben einen Algorithmus, der in O(|V| + |E|) dieSZK eines gerichteten Graphen [V,E] bestimmt.

Dieser Algorithmus kann mit der Konstruktiondes Transitionssystems verbunden werden:

FOR ALL [v,v’] in E DO....

FOR ALL commands g : g enabled in s DOs’ := execute g in s

....weiss noch nicht gesehen

30

Übung 1

Die Speisenden Philosophen.5 Philosophen sitzen im Kreis am Tisch. Zwischen jezwei Philosophen liegt eine Gabel. Philosophen denken oderessen. Um essen zu können, benötigen sie die beidenGabeln unmittelbar links und rechts von ihnen. Nach demEssen legen sie die Gabeln wieder ab (zwei benachbartePhilosphen können also nie gleichzeitig essen, weil sie eineGabel teilen).

1. Gib ein Transitionssystem an, das dieser Beschreibungentspricht und formuliere angemessene Fairnessannahmen!

2. Spezifiziere wünschenswerte Sicherheits- undLebendigkeitseigenschaften!

31

Übung 2

Für ein von Dir gewähltesTiefensuchszenario,

1. Ordne den Knoten diepassenden dfs-Nummern zu

2. Klassifiziere die Kanten

3. Bestimme die lowlink-Werte

4. Kennzeichne die SZK

32

Übung 3

Gib einen möglichst kleinen gerichteten Graphen an,der bei geeigneter Tiefensuchreihenfolgealle Kantentypen enthält (und bei Vorwärts- und Querkantenjeweils sowohl eine innerhalb einer SZK als auch eine zwischen verschiedenen SZK).