WIR

TS

CH

AF

TS

INF

OR

MA

TIK

WestfälischeWilhelms-Universität Münster

WIRTSCHAFTSINFORMATIK

Das Symbolic Model Verifier Das Symbolic Model Verifier (SMV) System (SMV) System

Präsentation im Rahmen des Seminars

„Ausgewählte Kapitel des Software Engineerings insb. Formale Spezifikation“

am 05.01.2006

Christian Ottenhof

2

WIRTSCHAFTSINFORMATIK

GliederungGliederung

1. Einleitung

2. Grundlagen des SMC

3. Das SMV System

4. Verifikation des Gigamax Protokolls

5. Zusammenfassung

3

WIRTSCHAFTSINFORMATIK

GliederungGliederung

1. Einleitung

2. Grundlagen des SMC

3. Das SMV System

4. Verifikation des Gigamax Protokolls

5. Zusammenfassung

4

WIRTSCHAFTSINFORMATIK

EinleitungEinleitung

Spezifikation: Anforderungen an ein formales Modell

Verifikation: Formal exakte Methode, um um die Konsistenz zwischen

Modell und Spezifikation für alle Eingabedaten zu beweisen

Spezifikation Modell

Spez. falsch Spez. korrekt

Verifikation

5

WIRTSCHAFTSINFORMATIK

EinleitungEinleitung

Modell kann verifiziert werden durch:

• Simulation

• Testen

• Formale Beweise (z.B. Induktion)

• Symbolisches Model Checking (SMC)

6

WIRTSCHAFTSINFORMATIK

GliederungGliederung

1. Einleitung

2. Grundlagen des SMC

3. Das SMV System

4. Verifikation des Gigamax Protokolls

5. Zusammenfassung

7

WIRTSCHAFTSINFORMATIK

Grundlagen des SMCGrundlagen des SMC

1. Kripke Struktur

Repräsentiert das formale Modell

2. Temporale CTL Logik

Notwendig um die Spezifikation zu formulieren

3. OBDD´s

Für die effiziente Verarbeitung von Booleschen Funktionen

8

WIRTSCHAFTSINFORMATIK

Grundlagen des SMCGrundlagen des SMCKripke StrukturKripke Struktur

Bestehend aus dem Tupel M = ( S, R, L )

S : Menge der Systemzustände

R : Übergangsrelation

L : Labelfunktion weist die Zustandsprädikate ai zu

S0

S1

S2

S3

{ a1,a2 }

{ a2 }

{ a2 }

9

WIRTSCHAFTSINFORMATIK

Grundlagen des SMCGrundlagen des SMCKripke StrukturKripke Struktur

Die Kripke Struktur kann auch als Baum dargestellt werden:

S0

S1

S2 S1

S2

S3 S3

S2

S3

S1

Eine Spezifikation ist somit eine Anforderung an den Baum der Kripke Struktur

10

WIRTSCHAFTSINFORMATIK

Grundlagen des SMCGrundlagen des SMCCTL LogikCTL Logik

Spezifikation des Modells wird in CTL formuliert:

AG(x) Die Formel x gilt auf allen Pfaden in allen Folgezuständen

AF(x) Die Formel x gilt auf allen Pfaden irgendwann

EG(x) Die Formel x gilt auf mind. einem Pfad in allen Folgezuständen

EF(x) Die Formel x gilt auf mind. einem Pfad irgendwann

x x x

x x x

x

x x x

x

x x

AG(x) AF(x) EG(x) EF(x)

11

WIRTSCHAFTSINFORMATIK

Grundlagen des SMCGrundlagen des SMCKripke StrukturKripke Struktur

Problem :

Bei vielen Zuständen lässt sich die Kripke Struktur nicht mehr

effizient verifizieren

Lösung :

Das „state explosion problem“ kann durch eine symbolische Darstellung der

Kripke Struktur vermieden werden

Der Zustandsgraph wird nicht explizit aufgebaut, sondern durch Boolesche

Formeln symbolisch repräsentiert

Symbolisches Model Checking

12

WIRTSCHAFTSINFORMATIK

Grundlagen des SMCGrundlagen des SMCKripke StrukturKripke Struktur

S0

S1

S2

S3

{ a1,a2 }

{ a2 }

{ a2 }

Symbolische Umsetzung von (S, R, L):

Die Zustände werden binär kodiert

{(00); (01); (10); (11)}

Die Übergangsrelation R: B2n B

fR = 0001+0011+0111+1101+1111

Für jedes Zustandsprädikat ai gibt

es eine Boolesche Funktion Bn B

Im Beispiel 2 Funktionen:

fa1 = 01

fa2 = 01+10+11

Startzustand: fS0 = 00

13

WIRTSCHAFTSINFORMATIK

Grundlagen des SMCGrundlagen des SMCOBDD´sOBDD´s

Symbolisches Model Checking basiert auf Booleschen Formeln

OBDD´s bieten eine kompakte Darstellungsform

Es existieren effiziente Algorithmen

siehe Vortrag zu OBDD´s

14

WIRTSCHAFTSINFORMATIK

GliederungGliederung

1. Einleitung

2. Grundlagen des SMC

3. Das SMV System

4. Verifikation des Gigamax Protokolls

5. Zusammenfassung

15

WIRTSCHAFTSINFORMATIK

Das SMV SystemDas SMV System

Symbolic Model Verifier (SMV) System

Hauptsächlich entwickelt von K.L. McMillan

Entwickelt in den Cadence Berkeley Labs

Experimentelles Tool, das SMC Techniken verwendet

Dient zur Forschung, um Anwendungen für SMC zu entwickeln

16

WIRTSCHAFTSINFORMATIK

Das SMV SystemDas SMV System

Anforderungen an einen symbolischen Model Checker:

vollautomatische Verifikation

synchrone und asynchrone Systeme verifizierbar

Erstellung eines abstrakten oder sehr detaillierten Modells

Wiederverwendung von einmalig erstellten Modellteilen

Anwendbarkeit und Anerkennung in der Praxis

17

WIRTSCHAFTSINFORMATIK

Das SMV SystemDas SMV SystemAblauf der VerifikationAblauf der Verifikation

Erstellung des Modells in der

SMV Eingabesprache

Die Spezifikation

in CTL erstellen

Verifikation durch das

SMV System

true

false

18

WIRTSCHAFTSINFORMATIK

Das SMV SystemDas SMV SystemErstellung des ModellsErstellung des Modells

Beispiel: Mutual Exclusion Protokoll (MUTEX)

Eigenschaften eines MUTEX:

Es sind 2 asynchrone Prozesse vorhanden

Diese teilen sich einen kritischen Bereich

Dieser Bereich darf von nur einem Prozess betreten werden

Das MUTEX Protokoll soll diese exklusive Nutzung sicherstellen

19

WIRTSCHAFTSINFORMATIK

Das SMV SystemDas SMV SystemErstellung des ModellsErstellung des Modells

MODULE main

VARturn : boolean;p0: process p(0,turn);p1: process p(1,turn);

In der SMV Eingabesprache besteht ein MUTEX aus 2 Modulen:

Schlüsselwort process deklariert einen Prozess

Es wird auf das Modul p verwiesen

20

WIRTSCHAFTSINFORMATIK

Das SMV SystemDas SMV SystemErstellung des ModellsErstellung des Modells

21

WIRTSCHAFTSINFORMATIK

Das SMV SystemDas SMV SystemErstellung des ModellsErstellung des Modells

MODULE p (nr,turn)

VARstate: {non_critical, critical};

ASSIGNinit(state):= non_critical;next(state):= case

state = non_critical & !(turn = nr) : non_critical;state = non_critical & turn = nr : critical;state = critical: {critical, non_critical};

esac;

next(turn):= casestate = critical & next(state) = non_critical : !nr;1 : turn;

esac;

22

WIRTSCHAFTSINFORMATIK

Das SMV SystemDas SMV SystemErstellung des ModellsErstellung des Modells

Hinzufügen der Spezifikation zum main Modul:

MODULE mainVAR

turn : boolean;p0: process p(0,turn);p1: process p(1,turn);

SPECAG !(p0.state = critical & p1.state = critical)

23

WIRTSCHAFTSINFORMATIK

Das SMV SystemDas SMV SystemErgebnis der VerifikationErgebnis der Verifikation

24

WIRTSCHAFTSINFORMATIK

Das SMV SystemDas SMV System

Bislang sind uns folgende Deklarationen begegnet:

VAR

ASSIGN

INIT

NEXT

SPEC

Es gibt noch eine weitere wichtige Deklaration

DEFINE

Durch DEFINE können häufiger benutzte Ausdrücke kompakter beschrieben

werden:

DEFINECarry_out := value & carry_in;

25

WIRTSCHAFTSINFORMATIK

GliederungGliederung

1. Einleitung

2. Grundlagen des SMC

3. Das SMV System

4. Verifikation des Gigamax Protokolls

5. Zusammenfassung

26

WIRTSCHAFTSINFORMATIK

Verifikation des Gigamax ProtokollsVerifikation des Gigamax Protokolls

Eigenschaften des Gigamax Multiprozessors:

Encore Computer Corporation

Verteilte Architektur

Reaktives System

„Simulierter“ Hauptspeicher

Das Cache Protokoll soll den

verteilten Speicher konsistent halten

UIC UIC

M P

UIC

M P

UIC

……

……

Globaler Bus

Lokaler Bus

27

WIRTSCHAFTSINFORMATIK

Verifikation des Gigamax ProtokollsVerifikation des Gigamax Protokolls

Architektur des Systems:

UIC UIC

M P

UIC

M P

UIC

……

……

Globaler Bus

Lokaler Bus

28

WIRTSCHAFTSINFORMATIK

Verifikation des Gigamax ProtokollsVerifikation des Gigamax Protokolls

In Fokus der Verifikation: Ein expliziter Speicherblock

Speicherblock im Cache „hit“

Speicherblock nicht im Cache „miss“

• In diesem Fall : Hauptspeicherzugriff

• Inhalte müssen aber konsistent gehalten werden

Im Folgenden: Abstrakte und modellhafte Umsetzung des

Cache Protokolls in der SMV Eingabesprache

29

WIRTSCHAFTSINFORMATIK

Verifikation des Gigamax ProtokollsVerifikation des Gigamax Protokolls

Erstellung von 3 Modulen mit den zugehörigen Variablen:

module cache-device

• state (Zustand aus Sicht des Caches)

• snoop (boolesche Variable)

module bus-device

• master (Bus Master)

• cmd (Befehle)

• waiting (boolesche Variable)

module processor

30

WIRTSCHAFTSINFORMATIK

Verifikation des Gigamax ProtokollsVerifikation des Gigamax Protokolls

Ein Speicherblock kann aus Sicht des Caches die folgenden Zustände haben:

owned ( read und write möglich)

shared ( nur read möglich)

invalid ( nicht im Cache vorhanden)

In der SMV Eingabesprache:

MODULE cache-device VAR state : {invalid,shared,owned};  DEFINE readable := ((state = shared) | (state = owned)) & !waiting; writable := (state = owned) & !waiting;

31

WIRTSCHAFTSINFORMATIK

Verifikation des Gigamax ProtokollsVerifikation des Gigamax Protokolls

Bei jedem Bus Zyklus wird ein Master bestimmt

Alle anderen Einheiten werden als Slaves behandelt

Der Bus Master kann einen der folgenden Basisbefehle auf den Bus senden:

read : Bestehend aus einer Anfrage für einen bestimmten Speicherblock.Wird durch einen response Befehl beantwortet.

write : Speichert die Daten eines bestimmten Speicherblock im Hauptspeicher des Clusters.

write/resp: Sendet den durch read angeforderten Speicherblock an den Anfrager und speichert den Block im Hauptspeicher.

32

WIRTSCHAFTSINFORMATIK

Verifikation des Gigamax ProtokollsVerifikation des Gigamax Protokolls

In Abhängigkeit vom gesendeten Befehl, ist der Folgezustand des Bus

Masters festgelegt:

akt. Zustand Befehl Folgezustand Grund

invalid read-shared shared read missinvalid or shared read owned owned write missowned write-invalid invalid copy-backowned write-resp-invalid invalid snoop read-ownedowned write-shared shared write-troughowned write-resp-shared invalid snoop read-shared

33

WIRTSCHAFTSINFORMATIK

Verifikation des Gigamax ProtokollsVerifikation des Gigamax Protokolls

Zustandsübergänge in der SMV Eingabesprache:ASSIGN init(state) := invalid; next(state) := case abort : state; master : case CMD = read-shared : shared; CMD = read-owned : owned; CMD = write-invalid : invalid; CMD = write-resp-invalid : invalid; CMD = write-shared : shared; CMD = write-resp-shared : shared; 1 : state; esac; !master & state = shared & (CMD = read-owned | CMD = invalidate) : invalid;  state = shared : {shared,invalid}; 1 : state ;esac;

34

WIRTSCHAFTSINFORMATIK

Verifikation des Gigamax ProtokollsVerifikation des Gigamax Protokolls

Alle Slaves hören den Bus ab und antworten auf den Befehl des Masters:

reply-waiting (Slave wartet auf einen Block, ein read des Bus Masters würde vernichtet)

reply-owned (veranlasst ein write/resp, snoop Variable wird gesetzt )

reply-stall (Slave kann nicht antworten)

DEFINE reply-waiting := !master & waiting;

DEFINE reply-owned := !master & state = owned;

35

WIRTSCHAFTSINFORMATIK

Verifikation des Gigamax ProtokollsVerifikation des Gigamax Protokolls

Zustandsübergänge der snoop Variable

VAR snoop : boolean; ASSIGN init(snoop) := 0; next(snoop) := case abort : snoop;

state = owned & CMD = read-shared : 1;state = owned & CMD = read-owned : 1;CMD = write-resp-invalid : 0;

CMD = write-resp-shared : 0; 1 : snoop; esac;

36

WIRTSCHAFTSINFORMATIK

Verifikation des Gigamax ProtokollsVerifikation des Gigamax Protokolls

MODULE bus-device VAR master : boolean; cmd : {idle,read-shared,read-owned,write-invalid,write-shared,

write-resp-invalid,write-resp-shared,invalidate,response}; waiting : boolean; reply-stall : boolean; ASSIGN init(waiting) := 0; next(waiting) := case abort : waiting; master & CMD = read-shared : 1; master & CMD = read-owned : 1; !master & CMD = response : 0; !master & CMD = write-resp-invalid : 0; !master & CMD = write-resp-shared : 0; 1 : waiting; esac;

Zustandsübergänge der waiting Variable:

37

WIRTSCHAFTSINFORMATIK

Verifikation des Gigamax ProtokollsVerifikation des Gigamax Protokolls

Befehle die der Bus Master senden darf:

MODULE processor(CMD,REPLY-OWNED,REPLY-WAITING,REPLY-STALL)

 ASSIGN cmd := case master & state = invalid : {read-shared,read-owned}; master & state = shared & !waiting : read-owned; master & snoop & state = invalid : write-resp-invalid; master & snoop & state = shared : write-resp-shared; master & state = owned & !waiting : write-invalid; 1 : idle; esac;

38

WIRTSCHAFTSINFORMATIK

Verifikation des Gigamax ProtokollsVerifikation des Gigamax Protokolls

Zusätzlich müssten noch die UIC Schnittstellen modelliert werden

Diese können „local“ oder „remote“ sein

Die local UIC können als Sender oder Empfänger fungieren

UIC UIC

M P

UIC

M P

UIC

……

……

Globaler Bus

Lokaler Bus

39

WIRTSCHAFTSINFORMATIK

Verifikation des Gigamax ProtokollsVerifikation des Gigamax Protokolls

Überprüfung des Protokolls auf Deadlocks:

Das erstellte Modell muss der folgenden Spezifikation genügen

Zu jeder Zeit muss der explizit betrachtete Speicherblock die Möglichkeit

haben „writeable“ und auch wieder „readable“ zu werden

SPECAG(EF readable & EF writeable)

40

WIRTSCHAFTSINFORMATIK

Verifikation des Gigamax ProtokollsVerifikation des Gigamax Protokolls

Ergebnis der Verifikation mit dem SMV System:

Das SMV System fand heraus, dass die Spezifikation nicht korrekt ist

Die Entwickler des Systems haben den Deadlock durch Simulation nicht finden können

Eine sehr komplexe Abfolge von 14 Schritten führt zu einem Deadlock

Durch Analyse der Schrittfolge zum Deadlock, konnte der Fehler im Gigamax Protokoll behoben werden

41

WIRTSCHAFTSINFORMATIK

GliederungGliederung

1. Einleitung

2. Grundlagen des SMC

3. Das SMV System

4. Verifikation des Gigamax Protokolls

5. Zusammenfassung

42

WIRTSCHAFTSINFORMATIK

ZusammenfassungZusammenfassung

Symbolisches Model Checking ermöglicht vollautomatische Verifikation

Mit dem SMV System ist die Abstraktionsebene frei wählbar

Wiederverwendung von Modulen erspart Kosten

Es können komplexe Fehler entdeckt werden

Aber auch das SMC kann an seine Grenzen stoßen

43

WIRTSCHAFTSINFORMATIK

Vielen Dank

für die

Aufmerksamkeit !

44

WIRTSCHAFTSINFORMATIK