Date post: | 05-Apr-2015 |
Category: |
Documents |
Upload: | christianne-schierer |
View: | 106 times |
Download: | 2 times |
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