WIRTSCHAFTSINFORMATIK Westfälische Wilhelms-Universität Münster WIRTSCHAFTS INFORMATIK Das...

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


GliederungGliederung

1. Einleitung

2. Grundlagen des SMC

3. Das SMV System

4. Verifikation des Gigamax Protokolls

5. Zusammenfassung

3



1. Einleitung


3. Das SMV System


5. Zusammenfassung

4


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


EinleitungEinleitung

Modell kann verifiziert werden durch:

• Simulation

• Testen

• Formale Beweise (z.B. Induktion)

• Symbolisches Model Checking (SMC)

6



1. Einleitung


3. Das SMV System


5. Zusammenfassung

7


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


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



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


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



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



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


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



1. Einleitung


3. Das SMV System


5. Zusammenfassung

15


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



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


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


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



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



21



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



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


Das SMV SystemDas SMV SystemErgebnis der VerifikationErgebnis der Verifikation

24



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



1. Einleitung


3. Das SMV System


5. Zusammenfassung

26


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



Architektur des Systems:

UIC UIC

M P

UIC

M P

UIC

……

……

Globaler Bus

Lokaler Bus

28



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



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



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



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



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



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



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



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



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



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



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



Ü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



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



1. Einleitung


3. Das SMV System


5. Zusammenfassung

42


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


Vielen Dank

für die

Aufmerksamkeit !

44


WIRTSCHAFTSINFORMATIK Westfälische Wilhelms-Universität Münster WIRTSCHAFTS INFORMATIK Das...

Documents

Transcript of WIRTSCHAFTSINFORMATIK Westfälische Wilhelms-Universität Münster WIRTSCHAFTS INFORMATIK Das...