WIRTSCHAFTSINFORMATIK Westfälische Wilhelms-Universität Münster WIRTSCHAFTS INFORMATIK...
-
Upload
lubbert-apitz -
Category
Documents
-
view
104 -
download
0
Transcript of WIRTSCHAFTSINFORMATIK Westfälische Wilhelms-Universität Münster WIRTSCHAFTS INFORMATIK...
WIR
TS
CH
AF
TS
INF
OR
MA
TIK
WestfälischeWilhelms-Universität Münster
WIRTSCHAFTSINFORMATIK
Symbolisches Model Checking Symbolisches Model Checking mit mit
Binary Decision DiagramsBinary Decision Diagrams
Im Rahmen des Seminars "Ausgewählte Kapitel des Software Engineering insb. Formale Spezifikation"
Andreas Jacobs
2
WIRTSCHAFTSINFORMATIK
GliederungGliederung
1. Motivation
2. Model Checking
3. Binary Decision Diagrams
4. Symbolisches Model Checking
5. Fazit
3
WIRTSCHAFTSINFORMATIK
1. Motivation1. Motivation
Beweis der Korrektheit
Deduktive Verifikation
Model Checking
Verifikation von Hardware- und Softwaresystemen
Testfälle
Testen Simulation
- Unvollständigkeit+ einfache Verfahren+ große Erfahrung
- aufwendige Verfahren- bei kleinen Systemen
+ Beweis der Korrektheit
4
WIRTSCHAFTSINFORMATIK
1. Motivation1. Motivation
Warum Verifikation von Hardware- und Softwaresystemen?
Hardware- und Softwaresysteme finden immer größere Verbreitung Eingebettete Systeme (Handys, Autos, usw.)
Flächendeckende Verbreitung im betrieblichen Bereich
Abhängigkeit von den Systemen
Systeme werden immer komplexer Mooresches Gesetz
Betriebssystementwicklung
Fehler schwieriger zu finden
5
WIRTSCHAFTSINFORMATIK
1. Motivation1. Motivation
Pentium-Division (1994)
Fehler verursachen hohe Kosten
Ariane 5 (1996)
Die neue "Ariane 5 ESC-A" auf der Startrampe.(Foto: ESA)
Quelle: http://www.cpu-museum.de/?m=Intel&f=Pentium+P5
6
WIRTSCHAFTSINFORMATIK
GliederungGliederung
1. Motivation
2. Model Checking
2.1 Modellbildung2.2 Spezifikation2.3 Verifikation
3. Binary Decision Diagrams
4. Symbolisches Model Checking
5. Fazit
2. Model Checking
7
WIRTSCHAFTSINFORMATIK
2. Model Checking2. Model Checking
+ automatisch-bei Fehlern Ausgabe eines Fehlerpfades-kein Eingriff während des Algorithmus nötig
- endlicher Zustandraum
-state expolsion problem
8
WIRTSCHAFTSINFORMATIK
2.1 Modellbildung2.1 Modellbildung
Sei AP eine Menge atomarer Aussagen. Als Kripke-Struktur wird ein Tripel M = (S, R, L) über AP bezeichnet mit
einer totalen Transitionsmenge R ⊆ S×S, so dass jeder Zustand s ∈ S einen Nachfolger t ∈ S in der Form hat, dass gilt R(s,t),
einer Funktion L, die jedem Zustand s ∈ S eine Menge der in s wahren atomaren Aussagen zuweist.
S als endliche Menge von Systemzuständen,
9
WIRTSCHAFTSINFORMATIK
2.1 Modellbildung2.1 Modellbildung
Ein Pfad mit einem Startzustand s ist eine unendliche Folge von Zuständen π = s0,s1,s2,s3,… , so dass s0 = s und R(si, si+1) für alle i ≥ 0 gilt.Beispielsweise s1,s2,s2,s5,s6,….
10
WIRTSCHAFTSINFORMATIK
2.1 Modellbildung2.1 Modellbildung
state explosion problem
Variable mit n Bits hat 2n Zustände.Bei n parallelen, unabhängigen Prozessen gibt es n! unterschiedliche
Ausführungsreihenfolgen.
Lösungsansätze:
Symbolische Darstellung der ZustandsmengePartial Order Reduction
11
WIRTSCHAFTSINFORMATIK
2.2 Spezifikation2.2 Spezifikation
Eine CTL Formel kann folgende Elemente enthalten:
Aussagevariablen (atomar): (vgl. Menge AP der Kripke-Struktur),
Boolesche Operatoren: ∧,∨,…(16 Operatoren),
Pfadquantoren: A (auf allen Pfaden gilt), E (auf mindestens einem Pfad gilt),
temporale Operatoren: X (Nachfolger), F (zukünftig), G (immer), U (bis) und R (Komplement zu U).
Auf einen Pfadquantor folgt immer ein temporaler Operator und alle 10 Kombinationen lassen sich durch EX, EG und EU ausdrücken.
12
WIRTSCHAFTSINFORMATIK
2.2 Spezifikation2.2 Spezifikation
CTL Formeln
13
WIRTSCHAFTSINFORMATIK
2.3 Verifikation2.3 Verifikation
2. Model Checking
2.1 Modellbildung: Kripke-Struktur
2.2 Spezifikation: CTL Formel
2.3 Verifikation
2.3.1 Fixpunkte
2.3.2 kleinste/größte Fixpunkte
2.3.3 CTL Model Checking
2.3 Verifikation
Es muss ein Algorithmus definiert werden, mit dem man in der Lage ist zu prüfen, ob eine Kripke-Struktur einer CTL Formel genügt.
14
WIRTSCHAFTSINFORMATIK
2.3.1 Fixpunkte2.3.1 Fixpunkte
P
P ({s1,s2,s3}) bzgl. der Teilmengenrelation ⊆
15
WIRTSCHAFTSINFORMATIK
2.3.1 Fixpunkte2.3.1 Fixpunkte
16
WIRTSCHAFTSINFORMATIK
2.3.2 Kleinste / größte Fixpunkte2.3.2 Kleinste / größte Fixpunkte
17
WIRTSCHAFTSINFORMATIK
2.3.2 Kleinste / größte Fixpunkte2.3.2 Kleinste / größte Fixpunkte
18
WIRTSCHAFTSINFORMATIK
function getExtremeFixpoint(τ: Funktional,
Z{false,true}):Z;
begin
Z’ = τ(Z);
while(Z’≠Z)do
Z = Z’;
Z’ = τ(Z);
end while;
return(Z);
end function.
2.3.3 CTL Model Checking2.3.3 CTL Model Checking
19
WIRTSCHAFTSINFORMATIK
Z = {s1,s2,s3,s4,s5,s6}Z = {s1,s2,s3,s5}
Z = trueZ’= τ(true)Z’= τ(τ(true))Z’= τ(τ(τ(true)))
Z = {s1,s2,s3}
2.3.3 CTL Model Checking: Beispiel 12.3.3 CTL Model Checking: Beispiel 1
s1 s2 s3
s4 s5 s6
Z = true;
while(Z’≠Z)do
return(Z);
Z’= τ(Z);
Z = Z’;
Z’ = τ(Z);
end while;
≠
p p
p r
p,r
==
τ =
EG p
20
WIRTSCHAFTSINFORMATIK
2.3.3 CTL Model Checking: Beispiel 22.3.3 CTL Model Checking: Beispiel 2
1.HalloHalloHalloHalloHallo
2.HalloHalloHalloHalloHallo
3.HalloHalloHalloHalloHallo
4.HalloHalloHalloHalloHallo
E[p U r] =
21
WIRTSCHAFTSINFORMATIK
GliederungGliederung
1. Motivation
2. Model Checking
3. Binary Decision Diagrams
3.1 Ordered Binary Decision Diagrams3.2 Operationen auf OBDDs3.3 Komplexitätsbetrachtungen
4. Symbolisches Model Checking
5. Fazit
3. Binary Decision Diagrams
22
WIRTSCHAFTSINFORMATIK
3.1 Ordered Binary Decision Diagrams3.1 Ordered Binary Decision Diagrams
3. Binary Decision Diagrams
3.1 Ordered Binary Decision Diagrams
3.1.1 Definition Binary Decision Diagrams
3.1.2 Ordnung und Reduktion
3.1.3 Problem der Variablenordnung
3.2 Operationen auf OBDDs
3.3 Komplexitätsbetrachtungen
3.1 Ordered Binary Decision Diagrams
23
WIRTSCHAFTSINFORMATIK
3.1.1 Definition Binary Decision Diagram3.1.1 Definition Binary Decision Diagram
1 2 3f (x x ) x
Ein Binary Decision Diagram (BDD) stellt eine Boolesche Funktion als einen gerichteten, azyklischen Graphen dar.
Alle Endknoten (Blätter) sind entweder mit 0 oder 1 markiert.
Jeder andere Knoten k repräsentiert eine binäre Variable xi
und hat genau zwei Nachfolger:- lo(k), wenn xi=0- hi(k), wenn xi=1
24
WIRTSCHAFTSINFORMATIK
3.1.2 Ordnung und Reduktion3.1.2 Ordnung und Reduktion
Ordered BDD (Randal E. Bryant 1986)
1.Ordnung des BDD -> OBDD
2.Reduktion des OBDD -> (Reduced) OBDD
Effiziente Darstellung von (vielen) Booleschen Funktionen durch zwei Einschränkungen auf BDDs:
25
WIRTSCHAFTSINFORMATIK
3.1.2 Ordnung und Reduktion3.1.2 Ordnung und Reduktion
1. Ordnungtotale Ordnung auf die Menge der Variablen, so dass für jeden Knoten k mit dem Wert xi gilt:
- ∄ n ∈ {lo(k), hi(k)} mit xj, dass gilt: i,j ∈1..n und j≥i
26
WIRTSCHAFTSINFORMATIK
3.1.2 Ordnung und Reduktion3.1.2 Ordnung und Reduktion
2. Reduktion (zwei Regeln)
verdeckung
27
WIRTSCHAFTSINFORMATIK
3.1.2 Ordnung und Reduktion3.1.2 Ordnung und Reduktion
verdeckung
verdeckung verdeckung
Beispiel:
28
WIRTSCHAFTSINFORMATIK
3.1.2 Ordnung und Reduktion3.1.2 Ordnung und Reduktion
Ein Ordered Binary Decision Diagram (OBDD) stellt eine Boolesche Funktion als einen gerichteten, azyklischen Graphen dar, der sowohl geordnet als auch reduziert ist.
Genau ein Blatt hat den Wert 0, das andere den Wert 1.
Jeder andere Knoten k repräsentiert eine binäre Variable xi und hat genau zwei Nachfolger:
- lo(k), wenn xi=0- hi(k), wenn xi=1
Ein OBDD ist eine kanonische Darstellung einer Booleschen Funktion.
OBDD
29
WIRTSCHAFTSINFORMATIK
3.1.3 Problem der Variablenordnung3.1.3 Problem der Variablenordnung
1 1 2 2 3 3(a b ) (a b ) (a b ) OBDDs zu derselben Funktion
1 1 2 2 3 3a b a b a b 1 2 3 1 2 3a a a b b b
30
WIRTSCHAFTSINFORMATIK
3.1.3 Problem der Variablenordnung3.1.3 Problem der Variablenordnung
Sifting-Algorithmus
// Phase 1: Ermittlung der lokal besten Position von x2
// x2 steigt in Richtung der Blätter auf
// x2 sinkt in Richtung des Startknotens ab
// alle Positionen durchlaufen
x1
x1
x1
x1
x1
x2
x2
x3
x3
x3
x2
x1
x3
x2
x4
x2
x3
x3
x4
x4
x2
x4
x4
x4
x1<x2<x3<x4
swap(x2, x3)
swap(x2, x4)
swap(x4, x2)
swap(x3, x2)
swap(x1, x2)
// Phase 2: Aufsteigen zur besten Variablenordnung
// beste Variablenordnung erreicht: x1<x3<x2<x4
x1
x1
x2
x3
x3
x2
x4
x4
swap(x2, x1)
swap(x2, x3)
31
WIRTSCHAFTSINFORMATIK
3.2 Operationen auf OBDDs3.2 Operationen auf OBDDs
3. Binary Decision Diagrams
3.1 Ordered Binary Decision Diagrams
3.2 Operationen auf OBDDs
3.2.1 Negation
3.2.2 Apply
3.2.3 AndExists
3.3 Komplexitätsbetrachtungen
3.2 Operationen auf OBDDs
32
WIRTSCHAFTSINFORMATIK
3.2.1 Negation3.2.1 Negation
33
WIRTSCHAFTSINFORMATIK
3.2.2 Apply3.2.2 Apply
Verknüpfung zweier Boolescher Funktionen mit einembeliebigen zweistelligen Booleschen Operator:
1 n 1 n 1 n(f g)(x ,..., x ) f (x ,..., x ) g(x ,..., x )
34
WIRTSCHAFTSINFORMATIK
3.2.2 Apply3.2.2 Apply
i i i ii x 0 x 0 i x 1 x 1f g ( x (f g )) (x (f g ))
Gleiche Variablenordnung, rekursiv durch Shannon-Entwicklung
Fallunterscheidung beim Aufruf der OBDDs:
1. F und G sind Blätter -> Rekursion beendet
2. F und/oder G sind keine Blätter -> rekursiver Aufruf von Apply
2.1 Startknoten beider OBDD repräsentieren die gleiche Variable
2.2 Startknoten repräsentieren nicht die gleiche Variable
Apply-Algorithmus:
35
WIRTSCHAFTSINFORMATIK
3.2.2 Apply3.2.2 Apply
2.1: Beide Startknoten repräsentieren x1
Knoten mit x1 wird erzeugt.
Zwei rekursive Aufrufe von Apply.
36
WIRTSCHAFTSINFORMATIK
3.2.2 Apply3.2.2 Apply
2.2: F repräsentiert die „kleinere Variable“ x2
Knoten mit x2 wird erzeugt.
Zwei rekursive Aufrufe von Apply.
37
WIRTSCHAFTSINFORMATIK
3.2.2 Apply3.2.2 Apply
2.2: G repräsentiert die „kleinere Variable“ x3
Knoten mit x3 wird erzeugt.
Zwei rekursive Aufrufe von Apply.
38
WIRTSCHAFTSINFORMATIK
3.2.2 Apply3.2.2 Apply
1: F und G sind Blätter
Ein Blatt wird entsprechend dem Booleschen Operator erzeugt.
Apply wird mehr rekursiv aufgerufen.
39
WIRTSCHAFTSINFORMATIK
3.2.2 Apply3.2.2 Apply
1: F und G sind Blätter
Ein Blatt wird entsprechend dem Booleschen Operator erzeugt.
Apply wird mehr rekursiv aufgerufen.
40
WIRTSCHAFTSINFORMATIK
3.2.2 Apply3.2.2 Apply
2.1: Beide Startknoten repräsentieren x3
Knoten mit x3 wird erzeugt.
Zwei rekursive Aufrufe von Apply.
41
WIRTSCHAFTSINFORMATIK
3.2.2 Apply3.2.2 Apply
1: F und G sind Blätter
Es wird auf ein bereits berechnetes Ergebnis zurückgegriffen.
Kein rekursiver Aufruf von Apply.
42
WIRTSCHAFTSINFORMATIK
3.2.2 Apply3.2.2 Apply
1: F und G sind Blätter
Ein Blatt wird entsprechend dem Booleschen Operator erzeugt.
Kein rekursiver Aufruf von Apply.
43
WIRTSCHAFTSINFORMATIK
3.2.2 Apply3.2.2 Apply
2.2: F repräsentiert die „kleinere Variable“ x3
Ein Blatt wird entsprechend dem Booleschen Operator erzeugt.
Apply ist fertig. Das Ergebnis-OBDD ist nicht reduziert.
44
WIRTSCHAFTSINFORMATIK
3.2.2 Apply3.2.2 Apply
Komplexität von Apply: O(|F|*|G|)
Tricks:
1. Frühzeitige Auswertung
2. Hashtabelle zum Speichern der Berechnungen
45
WIRTSCHAFTSINFORMATIK
3.2.3 AndExists3.2.3 AndExists
existentielle Quantifizierung von Variablen
Für einen Vektor gilt:
x 0 x 1x.f f f
1 nx (x ,..., x )
na {false,true}
x.f ( x.f )(a)V
Für eine Boolesche Funktion ist die existenzielle Quantifizierung bezüglich der Variablen x definiert durch
46
WIRTSCHAFTSINFORMATIK
3.2.3 AndExists3.2.3 AndExists
AndExists funktioniert wie Apply mit der Konjunktion (∧) als Booleschen Operator.
Die einzige Änderung ist:
x 0 x 1x.f f f
47
WIRTSCHAFTSINFORMATIK
3.2.3 AndExists – Beispiel3.2.3 AndExists – Beispiel
48
WIRTSCHAFTSINFORMATIK
3.2.3 AndExists – Beispiel3.2.3 AndExists – Beispiel
49
WIRTSCHAFTSINFORMATIK
3.2.3 AndExists – Beispiel3.2.3 AndExists – Beispiel
50
WIRTSCHAFTSINFORMATIK
3.2.3 AndExists – Beispiel3.2.3 AndExists – Beispiel
51
WIRTSCHAFTSINFORMATIK
3.2.3 AndExists – Beispiel3.2.3 AndExists – Beispiel
52
WIRTSCHAFTSINFORMATIK
3.2.3 AndExists – Beispiel3.2.3 AndExists – Beispiel
Das Ergebnis von AndExists ist nicht reduziert.
53
WIRTSCHAFTSINFORMATIK
3.2.3 AndExists – Beispiel3.2.3 AndExists – Beispiel
54
WIRTSCHAFTSINFORMATIK
3.2.3 AndExists – Beispiel3.2.3 AndExists – Beispiel
55
WIRTSCHAFTSINFORMATIK
3.3 Komplexitätsbetrachtungen3.3 Komplexitätsbetrachtungen
3. Binary Decision Diagrams
3.1 Ordered Binary Decision Diagrams
3.2 Operationen auf OBDDs
3.3 Komplexitätsbetrachtungen
3.3.1 Darstellung Boolescher Funktionen als OBDDs
3.3.2 Operationen auf OBDDs
3.3 Komplexitätsbetrachtungen
56
WIRTSCHAFTSINFORMATIK
3.3.1 Darstellung Boolescher 3.3.1 Darstellung Boolescher Funktionen als OBDDsFunktionen als OBDDs
Funktionsklasse Komplexität
bester Fall schlechtester Fall
symmetrisch linear quadratisch
Integer Addition linear exponentiell
Integer Multiplikation exponentiell exponentiell
57
WIRTSCHAFTSINFORMATIK
3.3.2 Operationen auf OBDDs3.3.2 Operationen auf OBDDs
Algorithmus Komplexität
Reduktion von F proportional zur Knotenanzahl: O(F)
Variablenordnung mit Sifting O(n2) Vertauschungen zweier Variablen
Negation konstant (Vertauschung der Blätter)
Apply(F,G,*) quadratisch: O(|F|*|G|)
AndExists((x1,…,xn),F,G) exponentiell: O(|F|*|G|*22n)
58
WIRTSCHAFTSINFORMATIK
GliederungGliederung
1. Motivation
2. Model Checking
3. Binary Decision Diagrams
4. Symbolisches Model Checking
4.1 Modellbildung
4.2 Spezifikation
4.3 Verifikation
5. Fazit
4. Symbolisches Model Checking
59
WIRTSCHAFTSINFORMATIK
4.1 Modellbildung4.1 Modellbildung
Symbolische Darstellung der Kripke-Struktur
60
WIRTSCHAFTSINFORMATIK
4.1 Modellbildung4.1 Modellbildung
Ein Zustand kann durch einen Vektor Boolescher Werte ausgedrückt werden:
1 np (x ,..., x ).
Eine Menge von Zuständen kann eindeutig durch ein Funktional dargestellt werden:
z.B. s1 ≙ (0,0)
- OBDD p enthält nur die Variablen x1,…,xn
- p ist eine Menge von Booleschen Vektoren
p
M = (S, S0, R, L)
61
WIRTSCHAFTSINFORMATIK
4.1 Modellbildung4.1 Modellbildung
Beispiel zur Menge von Zuständen:1 np (x ,..., x ). p
2 1 2 1 2(x x ) (x x ) x
Boolescher Vektor (x2, x1):
= p
(1) ≙ Menge der Zustände, in denen r∈AP gilt.
M = (S, S0, R, L)
s3 und s4:
62
WIRTSCHAFTSINFORMATIK
4.1 Modellbildung4.1 Modellbildung
Ein Zustandsübergang wird durch ein Paar von Zuständen ausgedrückt:
Eine Menge von Zustandsübergängen kann eindeutig durch ein Funktional dargestellt werden:
z.B. (s1,s2)≙( (0,0), (0,1) )
- OBDD R enthält nur die Variablen x1,…, xn, x1´,…, xn´
- R ist eine Menge von Paaren Boolescher Vektoren
R
(s,s )
1 n 1 nR ((x ,..., x ), (x ,..., x )).
M = (S, S0, R, L)
63
WIRTSCHAFTSINFORMATIK
4.1 Modellbildung4.1 Modellbildung
M = (S, S0, R, L)
R1 n 1 nR ((x ,..., x ), (x ,..., x )).
R = ((s1,s2), (s2,s2), (s2,s3), (s3,s4))
≙
Überlagerung
64
WIRTSCHAFTSINFORMATIK
4.1 Modellbildung4.1 Modellbildung
Anhand einer atomaren Aussage wird ein OBDD mit denjenigen Zuständen zurückgegeben, in denen die Aussage gilt.
M = (S, S0, R, L)
2 1 2 1 2 1 2 2 1( x x ) ( x x ) (x x ) x (x x ) L(p) =
65
WIRTSCHAFTSINFORMATIK
4.2 Spezifikation4.2 Spezifikation
Zur Erinnerung:
66
WIRTSCHAFTSINFORMATIK
4.2 Spezifikation4.2 Spezifikation
Gesucht: CTL-Operator EX auf symbolischer Kripke-Struktur
Gegeben: EXp ≙ 1 n(x ,..., x ) x
1 n(x ,..., x ) x
Nachfolger
1 n 1 n((x ,..., x ), (x ,..., x )) Übergang
Lösung:
67
WIRTSCHAFTSINFORMATIK
4.2 Spezifikation4.2 Spezifikation
EXp x. x .(R(x, x ) p(x ))
1 np (x ,..., x ). p1 n 1 nR ((x ,..., x ), (x ,..., x )). R
EXp x. x .( )
R p
AndExists Algorithmus
68
WIRTSCHAFTSINFORMATIK
4.3 Verifikation4.3 Verifikation
Analyse der
Formel
AndExists
kleinster Fixpunkt
größter Fixpunkt
69
WIRTSCHAFTSINFORMATIK
4.3 Verifikation: Beispiel4.3 Verifikation: Beispiel
EG p
70
WIRTSCHAFTSINFORMATIK
4.3 Verifikation: Beispiel4.3 Verifikation: Beispiel
71
WIRTSCHAFTSINFORMATIK
4.3 Verifikation: Beispiel4.3 Verifikation: Beispiel
72
WIRTSCHAFTSINFORMATIK
4.3 Verifikation: Beispiel4.3 Verifikation: Beispiel
73
WIRTSCHAFTSINFORMATIK
4.3 Verifikation: Beispiel4.3 Verifikation: Beispiel
74
WIRTSCHAFTSINFORMATIK
4.3 Verifikation: Beispiel4.3 Verifikation: Beispiel
75
WIRTSCHAFTSINFORMATIK
4.3 Verifikation: Beispiel4.3 Verifikation: Beispiel
76
WIRTSCHAFTSINFORMATIK
GliederungGliederung
1. Motivation
2. Model Checking
3. Binary Decision Diagrams
4. Symbolisches Model Checking
5. Fazit5. Fazit
77
WIRTSCHAFTSINFORMATIK
5. Fazit5. Fazit
Der vorgestellte Algorithmus zum Symbolischen Model Checking
ist ein effizientes Verfahren zur automatischen Verifikation.
Grenzen des Model Checking:-endlicher Zustandsraum-state explosion problem
Symbolic Model Verifier (SMV) System in der Praxis-Cache-Protokoll im IEEE-Futurebus+ (1992)
bisherige Erfolge vor allem im Hardwarebereich und bei
Kommunikationsprotokollen
78
WIRTSCHAFTSINFORMATIK
5. Fazit5. Fazit
große Unternehmen aktiv im Bereich Model Checking-SLAM Projekt von Microsoft: Treiberverifikation bei Windows XP
aktuelle Forschungsrichtung: Software Model Checking
Verbesserungen notwendig
-einheitlicher Ansatz mit deduktiver Verifikation
79
WIRTSCHAFTSINFORMATIK
Vielen Dank für die Aufmerksamkeit!