1

Computergestützte Verifikation

31.5.2002

2

4.2 SAT-basiertes Model Checking

Ansatz: Übersetze das Model Checking Problem inein aussagenlogisches Erfüllbarkeitsproblem undlöse dieses.

Inhalt4.2.1 Ein effizienter SAT-Solver4.2.2 Noch ein effizienter SAT-Solver4.2.3 LTL Model Checking als SAT-Problem

3

4.2.1 SAT-Solver für CNF

(Suche nach erfüllender Belegung)

Ausgangspunkt: Algorithmus von Davis-Putnam aus den 60ern

(xyz) (¬xy) (¬yz) (¬x¬y¬z)

(y) (¬yz) (¬y¬z) (yz) (¬yz)

x ¬x decide

(z) (¬z) yunit

propagationz

leere Klauselmenge= SAT!

pure literalpropagation

z

()leere Klausel = Konflikt Backtracking zur letzten offenen Entscheidung

4

Davis-Putnam-Algorithmus

DP(K) K – Klauselmenge IF K = ø THEN RETURN SAT IF () K THEN RETURN UNSAT IF = ( ...1...) K THEN RETURN DP(K \ {}) IF (0...0[¬]xi) K THEN RETURN DP(K/ xi1[0]) IF K enthält Literal l, aber nicht seine Negation THEN RETURN DP(K \ { | l }) choose i IF DP(K/ xi 1) = SAT THEN RETURN SAT RETURN DP(K/ xi 0)

Tautologie

unit

pure literal

decide/backtrack

5

Dilemma rule

12

(x/0) (x/1)

1 2

Ableitung 1 Ableitung 2

= Eine der Subst., falls andere zu Konflikt führt;= diejenigen Subst., die in beiden Zweigen gleich sind, sonst

Zusammenführen derZweige Vermeideredundante Arbeit inverschiedenen Zweigen

6

Ableitungsstufen

Stufe 0 x

y

x

Stufe 1

x

Stufe 2

y z

z y

usw.

Stålmarcks Algorithmus:

for k = 0, ..., #Var doex.? Abl der Stufe k

end

7

Symbolische Pfade

Zustand mit Eigenschaft E ist von einem Zustand mit Eigenschaft I in genau k Schritten erreichbar:

I(x(0)) T(x(0),x(1)) ... T(x(k-1),x(k)) E(x(k))

Suche bis zum kleinsten k, das erfüllt

x(0) ...x(k)y(0)... y(j-1)

I(x(0)) T(x(0),x(1)) ... T(x(k-1),x(k))

[ I(y(0)) T(y(0),y(1)) ... T(y(j-1),x(k)) ]j<k

8

Beschränkte Semantik von LTL

Idee: beschreiben Gegenbeispiel der Länge k

1 k 1l

k

Ziel: Wenn beschränkter Pfad erfüllt, so auch jede unendlicheFortzsetzung

Lassopfade: beschr. Semantik = originale Semantikkreisfrei: k F i k: (i) k-i k G false

die anderen Operatoren so, wie man es sich denkt

9

Übersetzung der Semantik

I(x(0)) T(x(0),x(1)) ... T(x(k-1),x(k)) 0k

pik := p(x(i))

ik := i

k ik ¬ i

k := ¬ ik

G ik := false

F ik := j=i

k jk

X ik := falls i < k, dann i+1

k sonst false

U ik := j=i

k ( jk n=j

knk)

kreisfrei:

10

Übersetzung der Semantik

I(x(0)) T(x(0),x(1)) ... T(x(k-1),x(k)) T(x(k),x(l)) l = 0k l0

k

lpik := p(x(i))

lik := li

k ik l¬ i

k := ¬ l ik

lG ik := n=min(j,l)

klnk

lF ik := j=min(i,l)

k lj

k

lX ik := lk

succ(i) succ(i) = i+1 falls i < k, sonst l

lU ik := j=i

k (ljk n=j

j-1lnk)

j=li-1(lj

k n=jkln

k n=lj-1ln

k)

Lasso:

11

Zusammenfassung SAT

Es gibt inzwischen auch zustandsbasierte SAT-Model Checker

Man kann auf weitere Zuwächse im SAT-Solving vertrauen

Formeln für Bestimmung des max. k gelten als schwer meist wird auf Bestimmung oberer Schranken für k verzichtet unvollständige Methode

12

Zusammenfassung symbolisches Model Checking

Ideen für andere geeignete Datenstrukturen?

Symbolische Model Checker arbeiten gelegentlich mit Überapproximationen, d.h. einer Obermenge dererreichbaren Zustände, die Datenstruktur verkleinert

Industrielle Model Checker sind meist symbolisch

BDD und SAT-basierte Methode mischen sich –“Boolean Expression Diagrams”

13

Tools

SMV – “Symbolic Model Verifier”

BDD-basierte Tool-Familie

DAS Tool, das industrielle Aufmerksamkeit erregte

Viele Varianten zur Fixpunktberechnung, Variablenordnung...

Vor allem in der Hardwareverifikation verwendet

www-2.cs.cmu.edu/~modelcheck

www-cad.eecs.berkeley.edu/~kenmcmil/smv

14

Tools

BMC – “Bounded Model Checker”

übersetzt SMV-Input in SAT-Solver-lesbare Formeln

www-2.cs.cmu.edu/~modelcheck

15

Tools

NuSMV - bietet sowohl BDD- als auch SAT-basierteMethoden an

reimplementiert SMV und BMC

Eingabesprache weitgehend wie SMV

//nusmv.irst.itc.it

16

Anwendungen- IEEE FuturebusAnwendungen- IEEE Futurebus++

• 1992 Clarke + Studenten (CMU): Verifikation des IEEE Future+ cache coherence protocol mit SMV

• Es wurden mehrere vorher unerkannte Fehler entdeckt.

• Entwicklung des Protokolls begann 1988, ansonsten mit nur

informalen Methoden

17

Anwendungen-ISDN/ISUPAnwendungen-ISDN/ISUP

• NewCoRe Project (89-92) Softwareprojekt bei AT&T.

• Spezieller Model Checker bei der Entwicklung des CCITT ISDN User Part Protocol.

• 5 “verification engineers” analysierten 145 Requirements.

• Insgesamt 7,500 Zeilen SDL SourceCode

• 112 Fehler; rund 55% der ursprünglichen Requirements waren

logisch inkonsistent

18

Anwendungen-ErdbebensicherheitAnwendungen-Erdbebensicherheit

• 1995 (Concurrency Workbench) Analyse einer aktiven Strukturkomponente zur Erbebensicherung von Gebäuden.

• Messung von Kräften und hydrauliche Gegensteuerung, um Schwingungen abzufangen

• Ein Timing-Fehler wurde entdeckt, der die Schwingungen aufgeschaukelt hätte statt sie zu dämpfen.

19

ZusammenfassungFinite State Model Checking

2 Familien – explizit und symbolisch

explizit: gut bei verteilten, asynchron kommunizierendenSystemen mit wenig Datenabhängigkeit

symbolisch: gut, wenn wenig Nichtdeterminismus auftritt, (auch kein Nichtdeterminismus durch Verteiltheit)

Systeme “mit Struktur” tendieren zu guten BDD, SAT-Formeln

Experten nötig, um volle Power der Methoden auszuschöpfen

20

Kombination explizit-symbolisch

Versuche, Symmetrien oder Partial Order Reduction insymbolische Model Checker einubauen, führten zu mäßigemErfolg

explizit = gut bei Explosion in den Steuerstrukturensymbolisch = gut bei Explosion in Daten

vielleicht machbar: Steuervariablen explizit – Daten symbolisch?

21

Übung

Beschreibe per aussagenlogischer Formel einen Pfadaus 4 Zuständen, deren letzte 2 einen unendlichenZyklus bilden, und der die Formel G F für eineelementare Eigenschaft erfüllt.