1
Computergestützte Verifikation
25.6.2002
2
Probleme bei der Softwareverifikation
1. komplexe Datentypen und Expressions
2. Pointer und dynamische Datenstrukturen
3. Prozeduren und Rekursion
4. Bibliotheken
3
Idee von Abstract Interpretation
Rechnen im konkretem Verband Rechnen in einem “passenden” abstrakten Verband
Beispiele für abstrakte Verbände:
Zahlenintervalle [a,c][b,d] = [max(a,b),min(c,d)] [a,c][b,d] = [min(a,b),max(c,d)]
Boolesche Funktionen mit ,
Zonen mit Schnitt und konvexer Hülle der Vereinigung
Kreuzprodukte beliebiger Verbände (, komponentenweise)
4
“passend” = Galois-Verbindung
Konkret: [C,,] Abstrakt: [A,,]
Abstraktionsfunktion : C AKonkretisierungsfunktion : A C
() ist Galoisverbindung, wenn (x) Y gdw. x (Y)
Insbesondere: z ((z)) (x := z, Y := (z) ) ((Z)) Z (x := (Z)), Y := Z )
– “präziseste Abstraktion” – “liberalste Interpretation”
5
Widening
= Zwischenergebnis bei Fixpunktberechnung bewußt vergrößern
Vorteil: Terminierung in endlich vielen Schritten
Nachteil: berechneter Fixpunkt ist nicht notwendigerweise der kleinste
Beispiel: Widening: instabile Grenzen auf min(- 0,1)/max(0,1,)
[64,70] [32,71] [1, ] [0, ] [64,70] [63,71] [1, ] [0, ] [-, ]
6
Narrowing
= den durch Widening entstandenen Schaden begrenzen:
Def.: ist Narrowing falls
x y x y x y und für keine monoton fallende Kettex0, x1, ..., ist die Folgey0 := x0, yi+1 := yi x i+1 stark monoton fallend.
7
8.3 Shape Analysis
Ziel: Abstrakte Repräsentation von Invarianten dynamischer Datenstrukturen
Mittel: Abstrakte Interpretation auf geeigneter Domain
meist: “summary nodes”
x Liste mit mind. 1 Element
sm
8
Beispiel für Shape-Analysis
Insert in Liste:
x : nichtleere Liste x
malloc(y) xy
y -> n = x xy
x = y xy
Coarsening xy
9
Etwas schwieriger
Delete aus Liste
x: nichtleere Liste
Materialisierung
aus begleitenden Invarianten
dann einfach: y = x;
x = x -> n; free(y);
10
Begleitende Invarianten
sm(v) Location v repr. evt. mehr als ein Objektx(v) Variable x zeigt auf Objekt vn(v1,v2) v1.n zeigt auf v2
sh(v) mehr als ein Pointer zeigt auf vr(v) v ist von einer Variable erreichbar (kein Garbage)rx(v) v ist von x erreichbarc(v) v liegt auf einem Zykluscf.b(v) v.f -> b = &v (Doppellink)
...
alles interpretiert z.B. in 3-wertiger Logik (ja – vielleicht – nein)
11
8.4 Slicing
Ziel: Alle Programmteile streichen, die keinen Einfluß auf verifizierte Eigenschaft haben weniger Variablen (= kleinere Zustände) + weniger Übergänge
statisch: geg: Kriterium = (Variable, PC)
dynamisch: geg: Kriterium + Eingabe
12
Beispiel statisch
1 read(n);2 i := 1;3 sum := 0;4 product := 1;5 while i <= n do6 sum := sum + 1;7 product := product * i;8 i := i + 1; end9 write(sum);10 write(product);
(product,10)
1 read(n);2 i := 1;
4 product := 1;5 while i <= n do
7 product := product * i;8 i := i + 1; end
10 write(product);
13
Beispiel dynamisch
1 read(n);2 i := 1;3 while i <= n do4 if i mod 2 = 0 then5 x := 17; else6 x := 18;7 i := i + 1; end8 write(x);
(8,x,n=2)
1 read(n);2 i := 1;3 while i <= n do4 if i mod 2 = 0 then5 x := 17; else
7 i := i + 1; end8 write(x);
14
Kontrollflußgraph
start read(n) sum:=0 product:=1 i<=n
write sumwrite(product)stop
sum:=sum+1
product :=product*i
i:=i+1
15
Fluss-Abhängigkeit
x := ...
i j:=...x...
x DEF(i) x REF(i)x DEF(k)
j ist flussabhängig von i
16
Post-Dominanz
i ist post-dominiert von j falls jeder Kontrollpfad von izu STOP durch j geht
i if
j
17
Kontrollabhängigkeit
j von i kontrollabhängig falls-es gibt einen Pfad von i nach j, so daß jeder Knoten außer i von j post-dominiert ist- ist ist von j nicht post-dominiert
stop
i
jstop
while
i
j
18
Iterative Lösung von Datenflußgleichungen
R(i) – relevante Variablen in Knoten iS - relevante StatementsB - relevante Verzweigungen
R(i) += V falls Kriterium = (V,i)R(i) += {v} falls und entweder v R(j), v DEF(i), oder v REF(i), DEF(i) R(j)
i j
x :=
x := ...v...i j
v R(j)
x R(j)
19
Iterative ...
Startwert für S:
Alle Statements, die Variablen definieren, die bei einemdirekten Nachfolger relevant sind
v := v R(j)
20
Iterative....
Beispiel 1
1 v := 0;2 v := 1;3 x := v + 1;4 y := v + 2;5 output(v)
R
{}{}{v}{v}{v}
S: {2}
Beispiel 2 R
1 x:=0 {}2 y:= x+1 {x}3 v := x {x}4 z := v+1; {v}5 output(v) {v}
Kriterium(v,5)
S: {1,3}
21
Iterative....
B := Alle Branch-Statements, von denen ein relevantes Statement kontrollabhängig ist
dann:für alle b in B:R(b) += REF(b)
S += B
... und alles von vorn
22
Beispiel
1 v := 02 x := 53 if x < 7 then4 v := 15 output(v)
R(0)
{}{v}{v}{}{v}
Kriterium: (v,5)
S(0):{1,4}
B: {3}
R(1)
{}{v}{v,x}{}{v}
S(1):{1,2,3,4}
23
Zusammenfassung Softwareverifikation
essentiell: geeignete Abstraktion, Abstraktionsverfeinerung
Kombination Model Checking – Static Analysis - Alias-Analyse - Abstract Interpretation - Shape Analysis - Slicing
Viele Probleme, viele offen, aber auch Hoffnung
Unentscheidbarkeit setzt Grenzen
24
Tools
BANDERA
BEBOP, C2BP
JPF
.......
25
9. Sonstiges
Ziel: In einigen weiteren Domains Tragfähigkeit dergelernten Konzepte testen
26
9.1 Hybride Systeme
hybrid = kontinuierliche + diskrete Variablen
Hybrider Automat:
Einlaufen Auslaufen
h>= max
h <= minh’ [ -0.5,0.7]h’ [ -0.8,0.9]
(Der hier ist ein linearer Automat: x’ [c1,c2])
27
Hybrid vs. Timed vs Stopwatch
Timed Automata sind hybride Automaten:c’ = 1 in allen Zuständen
Stopwatch-Automata sind Hybride Automaten:c’ = 1 oder c’ = 0 in allen Zuständen
Erreichbarkeit für hybride Automaten unentscheidbar
28
Verifikation linearer hybrider Automaten
geometrische Abstraktionen, z.B. Polyeder – analog Zonen
mehrere andere geometrische Formen, u.a. Ellipsen
Tool:HyTech (Berkeley)
29
Verifikation allg. hybrider Automaten
numerische Verfahren Fehlerbetrachtung notwendig
Tool: CheckMate (CMU)
“Flowpipe”1
2
3
4
5
6
7
8
9
10
4 3,6,7