Download - Seminar Modellüberprüfung
![Page 1: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/1.jpg)
Seminar Modellüberprüfung
SMV – Symbolic Model Verifier
Referent: Markus Nosse
Inhaltsübersicht:
Grundlagen
Das SMV System
![Page 2: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/2.jpg)
Grundlagen – BDDs 1
Binäre Entscheidungsdiagramme Repräsentation von logischen Formeln Effiziente Algorithmen Kanonische Darstellungsform Repräsentation von Kripke Strukturen
![Page 3: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/3.jpg)
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
![Page 4: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/4.jpg)
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
![Page 5: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/5.jpg)
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
![Page 6: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/6.jpg)
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
![Page 7: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/7.jpg)
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)
![Page 8: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/8.jpg)
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
![Page 9: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/9.jpg)
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
![Page 10: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/10.jpg)
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]:
![Page 11: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/11.jpg)
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>)
![Page 12: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/12.jpg)
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
![Page 13: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/13.jpg)
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
![Page 14: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/14.jpg)
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; };
![Page 15: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/15.jpg)
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>
![Page 16: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/16.jpg)
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
![Page 17: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/17.jpg)
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
![Page 18: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/18.jpg)
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; };}
![Page 19: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/19.jpg)
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;
}
![Page 20: Seminar Modellüberprüfung](https://reader036.vdokument.com/reader036/viewer/2022082612/56813a64550346895da25e4a/html5/thumbnails/20.jpg)
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