Computergestützte Verifikation

(Halbkurs)

Karsten Schmidt

Di 9-11 R.3.113 Fr 15-17 R.4.101

Testen: kann nur die Anwesenheit von Fehlernfeststellen, nicht ihre Abwesenheit. (E. Dijkstra)

Verifikation: Nachweis der Korrektheit (theoretisch)

Fähigkeit, subtile Fehler zu finden (praktisch)

Konstruktion: Erzeugen des Systems aus derSpezifikation

Systematische Entwicklungsprozesse: z.B. ISO 9000

Anwendungsgebiete (Auswahl)

Safety critical systems (Autos, Flugzeuge, Atomkraftwerke...)

Mission critical systems (Raumsonden)

Hardware

Standards, Protokolle

Imageträchtige Software (MS Windows)

Tendenz wachsend.....

Verifikationstechniken

manuell

automatisch

Korrektheitsbeweis (z.B. Hoare-Kalkül)

interaktiv Theorembeweisen

Model Checking

Literatur

Konferenzen“Computer Aided Verification”(LNCS ...)

Skript meiner Vorlesung“Model Checking”~kschmidt/modelchecking/

Was ist Model Checking?

Erschöpfende Durchmusterung der Zustände einesSystems zur Prüfung einer vorgegebenen Eigenschaft

erster Ansatz: 1986

Durchbruch: 1992

inzwischen: einige Erfolgsstories, Einsatz in einigen Firmen, stetige Steigerung der Leistungsfähigkeit

Grundproblem: Zustandsexplosion

Zustandsexplosion

Wieviele Zustände kann man in welcher Zeitdurchmustern?Annahme: 800MHz, genug Speicher,ein neuer Zustand pro Prozessorzyklus

800,000,000 pro Sekunde48,000,000,000 pro Minute

2,880,000,000,000 pro Stunde69,120,000,000,000 pro Tag

25,246,080,000,000,000 pro Jahr

504,921,600,000,000,000,000,000,000 seit Urknall (< 1027)

Zustandsexplosion

Wie “groß” muß ein System sein, um 1027 Zustände zu haben?

Theoretisch reichen 80-90 boolesche Variablen

Praktisch reichen 200 boolesche Variablen (in verteilten Systemen)

Meilensteine der Technologie Model Checking:

1986: 106 1992: 1020 1996: 10100

2000: 101000

Model Checking: Prinzipskizze

System

Spezifikation Formalisierung log. Formel

Abstraktion Modell

Model Checker+

Gegenbeispiel

-

Simulation

VerfeinerungFehler-beseitigung

Präzisierung

Überlauf

Inhalt

System Abstraktion

Spezifikation

Simulation

Formalisierung

Model Checker

Gegenbeispiel

Modell

log. Formel

+

-

VerfeinerungFehler-beseitigung

Präzisierung

Überlauf

Kapitel 1: Systeme

Inhalt

System Abstraktion

Spezifikation

Simulation

Formalisierung

Model Checker

Gegenbeispiel

Modell

log. Formel

+

-

VerfeinerungFehler-beseitigung

Präzisierung

Überlauf

Kapitel 1: Systeme

Kapitel 2: Temporale Logik

Inhalt

System Abstraktion

Spezifikation

Simulation

Formalisierung

Model Checker

Gegenbeispiel

Modell

log. Formel

+

-

VerfeinerungFehler-beseitigung

Präzisierung

Überlauf

Kapitel 1: Systeme

Kapitel 2: Temporale Logik

Kapitel 3-k: Finite State Systems

Inhalt

System Abstraktion

Spezifikation

Simulation

Formalisierung

Model Checker

Gegenbeispiel

Modell

log. Formel

+

-

VerfeinerungFehler-beseitigung

Präzisierung

Überlauf

Kapitel 1: Systeme

Kapitel 2: Temporale Logik

Kapitel 3-k: Finite State SystemsKapitel (k+1)-n: Infinite State Sys.

Kapitel 1

Systeme

Zustand

Zusammenfassung aller Systemgrößen, die das weitereSystemverhalten wesentlich beeinflussen können

in der Regel beschrieben durch Zuordnung von Werten zuVariablen

Kreuzprodukt aller Wertebereiche = Zustandsraum

diskrete Systeme = alle Wertebereiche abzaehlbarkontinuierliche Systeme = alle Wertebereiche dichthybride Systeme = sowohl als auchreal-time Systeme = einzige kontinuierliche Größe ist die Zeitfinite state systems = Zustandsraum endlichinifinite state systems = Zustandsraum unendlich

Abstraktion

System

=

Zustandsraum S + Menge von Anfangszuständen I +Zustandsübergangsrelation E

kontinuierliche Systeme Differenzialgleichungendiskrete Systeme Teilmenge von S x A x S (A = Aktionen)hybride Systeme eine Differenzialgleichung pro Zustand der diskreten Variablen, plus diskrete Relation

Für diskrete Systeme: [S,I,A,E] = Transitionssystem

x,y: Nat

while x != y doif x < y then

y = y – xelse

x = x – yend

end

Beispiel für Transitionssystem

0

12

3

4

0;6,4 0;2,6

1;6,4 1;2,6

3;6,4 2;2,6

0;2,4

1;2,4

2;2,4

0;2,2

4;2,2

S = {0,1,2,3} x Nat x Nat

I = {0} x Nat x Nat

A = spaeter

E = irgendwie klar

Transitionssysteme sind einfach genug, allgemein genugals zugrundeliegendes theoretisches Konzept, aber ....

System Abstraktion

Spezifikation

Simulation

Formalisierung

Model Checker

Gegenbeispiel

Modell

log. Formel

+

-

VerfeinerungFehler-beseitigung

Präzisierung

Überlauf

... ungeeignet als Eingabesprache (wg. Zustandsexplosion)

... Programme auch ungeeignet, wg. zu komplexer Syntax

x,y: Nat

while x != y doif x < y then

y = y – xelse

x = x – yend

end

Eingabesprache 1: Guarded Commands

0

12

3

4

Var x,y: Nat pc: {0,1,2,3}

init(pc) = 0

pc = 0 & x = y pc = 4pc = 0 & x != y pc = 1pc = 1 & x < y pc = 2pc = 1 & x >= y pc = 3pc = 2 y = y – x, pc = 0pc = 3 x = x – y, pc = 0

Jedes guarded command bildet eine AktionEnabling: en(a) Teilmenge von S ( = guard liefert true)Zustandsübergang = wähle enabled guarded command undführe simultane Zuweisung aus

weitere Klassifikation von Systemen

sequentiell = jeder Zustand hat max. einen Nachfolgezst.deterministisch = pro Zustand und Aktion max. 1 Nachfolgezst.nichtdeterministisch = beliebig viele Nachfolgerverteilt = viele unabhängige Aktionen

Unabhängigkeitsrelation I zwischen Aktionen:

[a,b] in I gdw. keine der beiden Aktionen kann die Enabling-Bedingung der anderen ändern, und Resultat der Hinterein-anderausführung von a und b ist unabhängig von der Reihenfolge

s

s1

s2

s’

z.B. [g,g’] in I gdw. vorkommende Variablen disjunkt

Eingabesprache 2: Transitionsrelationen

Ursprung: Hardware

LogikRegister (n bits)

ri’ = fi(r1,...,rn,i1,...,im)

Input

Output

oj’ = fj(r1,...,rn,i1,...,im)

x,y: Nat

while x != y doif x < y then

y = y – xelse

x = x – yend

end

0

1

2

3

4

Var x,y: Nat pc: {0,1,2,3}

init(pc) = 0

next(pc) = switch(pc) case 0 : if x = y then 4 else 1

case 1 : if x < y then 2 else 3 case 2 : 0 case 3 : 0 else 4

next(x) = if pc = 3 then x – y else x

next(y) = if pc = 2 then y – x else y

alle Variablen werden simultan geändert; Aktionen = (z.B.)Werte der Eingabevariablen

Weitere Eingabesprachen

Petrinetze

Prozeßalgebren

Komposition von Transitionssystemen

Variablen-Transitionssysteme

Konstruktion des Transitionssystemsist Aufgabe des Model Checkers

Als Modell wird dem Model Checker eine implizite Systembeschreibung übergeben

Hinter jeder impliziten Beschreibung stecktein Transitionssystem

Zusammenfassung Kapitel 1

Es gibt viele Beschreibungssprachen

Übung 1:

Konstruiere das Transitionssystem zu folgendemProgramm (als guarded commands):

init(x1) = 1; init(x2) = 1, init(pc1) = 0, init(pc2) = 0, init(y) = 1

pc1 = 0 & y = 1 pc1 = 1, y = 0pc2 = 0 & y = 1 pc2 = 1, y = 0pc1 = 1 x1 = - x1 , pc1 = 2pc2 = 1 x2 = -x2 , pc2 = 2pc1 = 2 y = 1, pc1 = 0pc2 = 2 y = 1, pc2 = 0

Übung 2:

Ein 3-bit-Counter hat 3 Bits als Zustandsvariablen, die eineZahl zwischen 0 und 7 im Binärkode repräsentieren.Der Counter soll pro Takt um eine Zahl weiterzählen, wobeider Nachfolger der 7 wieder die Null sein soll. Anfangszustandsei die Null.Beschreibe dieses Verhalten als Nextstate-Programm mitdrei booleschen Variablen!

Übung 3:

Gegeben sei folgendes Transitionssystem (Zustände sind Knoten,Ereignisse sind durch Kanten zwischen Knoten repräsentiert,die mit Aktionen beschriftet sind). Gib die größtmöglichesymmetrische und irreflexive Relation zwischen Aktionen an, die die Eigenschaften einer Unabhängigkeitsrelation erfüllt!

b

c

d

a

c

d

a

c

d

a

c

d

a

f

f

f

f

g

g

g

g

e

e

e

e