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