seminar modellüberprüfung
Post on 05-Jan-2016
17 Views
Preview:
DESCRIPTION
TRANSCRIPT
Seminar Modellüberprüfung
SMV – Symbolic Model Verifier
Referent: Markus Nosse
Inhaltsübersicht:
Grundlagen
Das SMV System
Grundlagen – BDDs 1
Binäre Entscheidungsdiagramme Repräsentation von logischen Formeln Effiziente Algorithmen Kanonische Darstellungsform Repräsentation von Kripke Strukturen
Grundlagen – BDDs 2
Entscheidungsbaum Entscheidungsdiagramm ist (sehr viel) kompakter Beispiel: f = a b c
a
b b
c c c c
0 1
0 01 1
1 10 11 01 0
0 10 1 0 1 0 1
1
32
a
01
c
0 1
1 0
b0
1
Grundlagen – BDDs 3
Zusammenfassen isomorpher Teilbäume Terminale Knoten var(v1) = var(v2) und
low(v1) = low(v2) und high(v1) = high(v2)
Elimination überflüssiger Entscheidungen low(v) = high(v)
b
c c
0
1 01 0
0 1 0 1
1
2
c
1 1
0 1
Grundlagen – BDDs 4
Direkte Konstruktion mittels Shannon Expansion f(x1,...,xn) = (xif1) ( xi f0),
fk = f(x1,...,xi=k,...,xn ), k = 0,1
Pro Anwendung ein Knoten für xi
Teilbäume ergeben sich rekursiv aus f0, f1
a0 1
b cc
a b c
b0 1
a0 1
c
a b c
1c
b01
a0
1
a b c
1
c
0
01
b c
Grundlagen - OBDDs
Ordnung auf Variablen Minimalität, Kanonität Effiziente Algorithmen
Reduce – Minimierung mit Aufwand O(|G|log|G|)Apply – Logische Verknüpfung in O(|G||H|)Restrict – Shannon Expansion in O(|G|log|G|)
Optimale Ordnung coNP vollständiges Problem Ausreichend gute Ordnungen sind bestimmbar
Grundlagen - Repräsentation
Kripke-Strukturen als OBDDs Binäre Codierung der Zustandsvariablen Codierte Übergangsrelation definiert über {0,1} Charakteristische Funktion ist logische Formel Darstellbar als OBDD
a b a b
s1 s2
s1 s2: (a b) a’ b’)s2 s1: (a b) a’ b’)s2 s2: (a b) a’ b’)
(s1s2) (s2s1) (s2s2)
Symbolische Modellüberprüfung 1
Algorithmus Check Eingabe: CTL Formel Ausgabe: Menge der erfüllenden Zustände als
OBDD Bezug auf eine Kripke Struktur (S,R,L),
Übergangsrelation R liegt als OBDD vor
Symbolische Modellüberprüfung 2
Rekursive Definition über der Struktur von CTL Formeln Atomare Aussage f = a
Ergebnis ist Menge der Zustände, in denen a erfüllt ist
Boolesche Operatoren f = f1 f2, f = f1 Berechnung mittels Apply Operanden sind Check(f1) und Check(f2)
CTL Operator EX f Subroutine CheckEX Parameter ist Check(f) Ergebnis ergibt sich aus Relational Product Computation
Symbolische Modellüberprüfung 3
CTL Operator EG f Subroutine CheckEG Parameter ist Check(f) Berechnung über größten Fixpunkt
CTL Operator E[f U g] Subroutine CheckEU Parameter sind Check(f), Check(g) Berechnung über kleinsten Fixpunkt
p p
q
p p
q
p p
q
p p
q
E[p U q]:
SMV – Überblick 1
SMV – Symbolic Model Verifier Basistypen
Boolean Endliche Integer Intervalle Aufzählungstypen Syntaktische Abkürzungen für CTL Formeln
Signale Im Sinne von „Variablen“ Definition als <name> : <typ> Eindeutige Zuweisungen, keine zirkulären Abhängigkeiten Operatoren init(<signal>) und next(<signal>)
SMV - Überblick 2
Module Unterstützung von komponentenorientieren Modellen Mehrfach instanziierbar Parametrisierbar
Eingabe- und Ausgabeparameter Synchrone oder asynchrone Modellierung
Prozesse Schlüsselwort process Analogie: Prozessmodell auf Einprozessorsystem
SMV – Überblick 3
Spezifikation Mittels CTL Formeln Temporale Operatoren X, G, F und U
neXt, Globally, in the Future, Until Implizite universelle Quantifizierung Gegenbeispiele Voraussetzungen für Beweise
using … prove Annahme von nichtbeweisbaren Eigenschaften
assume … Fairness-Bedingungen
Weitere Sprachkonstrukte 1
Alles syntaktische Abkürzungen Komplexe Typen
Arrays Mit beliebigem Typ, auch n-dimensional oder generisch Index aufsteigend (0..7) oder absteigend (7..0) Bsp: proc: array[0..1];
bits: array[7..0] of boolean; Strukturierte Typen
Definition über Module Ausnahme: Strukturen ohne Parameter Bsp: hands : struct { left, right: boolean; };
Weitere Sprachkonstrukte 2
If Anweisung if (<expr>) <stmt1> [ else <stmt2> ] Statements analog zu C oder Java Bsp: if (test) a = 1; else b = 1;
Default Regeln Zustand des modellierten Systems entspricht Belegung
der Zustandsvariablen Semantik undefinierter Zustandsvariablen? Defaults bestimmen Werte für undefinierte Variablen Explizite Regeln definierbar
default <stmt1> in <stmt2>
Weitere Sprachkonstrukte 3
Case und Switch Anweisung Syntactic Sugar für if-else-Kaskaden
Schleifen Sogenannte Konstruktor Loops
werden zur Compilezeit ausgewertet und komplett ausgerollt
Fortgeschrittene Modellierung
Modellierung in Schichten Bessere Abstraktion möglich
Ausnutzen von Symmetrien Verifikation von “Repräsentanten” Anlehnung an Induktionsbeweise
Bewertung Mächtige Konzepte Fehlerträchtige Modellierung wegen Komplexität
Beispiel Mutex
MODULE proc(state, otherState) { output state: stateSet; input otherState: stateSet; init(state) := noncritical;
case { (state = noncritical) : next(state) := {trying, noncritical}; (state = trying) & (otherState = noncritical) : next(state) := critical; (state = trying) & (otherState = trying) : next(state) := critical; (state = critical) : next(state) := {critical, noncritical}; default: next(state) := state; };}
Beispiel Mutex
typedef stateSet {noncritical, trying, critical};
MODULE main() {
proc: array 0..1;
for(i=0; i<2; i = i+1)
proc[i] : process proc(proc[(i+1) mod 2].otherState,
proc[(i+1) mod 2].state);
fairness: assert G F proc[0].running & G F proc[1].running;
proc0_fair: assert G F ~(proc[0].state = critical);
proc1_fair: assert G F ~(proc[1].state = critical);
mutex_violation: assert G F ~((proc[0].state = critical) &
(proc[1].state = critical));
using fairness, proc0_fair, proc1_fair
prove mutex_violation;
assume fairness, proc0_fair, proc1_fair;
}
Bewertung und Stellungnahme
Praxistauglich Siehe Verifikation des FutureBus+
Kommerzielle Tools verfügbar, deutet auf industriellen Einsatz hin
SMV scheint hardwarelastig zu sein Interessante Technologie, aber
Theorie nicht leicht Modellierung auch nicht leicht
top related