x 2 - Universität Münster

 Datenstruktur

 140 views
of 79
All materials on our website are shared by users. If you have any questions about copyright issues, please report us to resolve them. We are always happy to assist you.
Description
Westfälische Wilhelms-Universität WIRTSCHAFTS Münster INFORMATIK Symbolisches Model Checking WIRTSCHAFTSINFORMATIK mit Binary Decision Diagrams Im Rahmen des…
Share
Transcript
Westfälische Wilhelms-Universität WIRTSCHAFTS Münster INFORMATIK Symbolisches Model Checking WIRTSCHAFTSINFORMATIK mit Binary Decision Diagrams Im Rahmen des Seminars "Ausgewählte Kapitel des Software Engineering insb. Formale Spezifikation" Andreas Jacobs WIRTSCHAFTS Gliederung INFORMATIK 1. Motivation 2. Model Checking 3. Binary Decision Diagrams 4. Symbolisches Model Checking 5. Fazit 2 WIRTSCHAFTS 1. Motivation INFORMATIK Verifikation von Hardware- und Softwaresystemen Testfälle Beweis der Korrektheit  Testen  Deduktive Verifikation  Simulation  Model Checking - Unvollständigkeit - aufwendige Verfahren + einfache Verfahren - bei kleinen Systemen + große Erfahrung + Beweis der Korrektheit 3 WIRTSCHAFTS 1. Motivation INFORMATIK Warum Verifikation von Hardware- und Softwaresystemen?  Hardware- und Softwaresysteme finden immer größere Verbreitung - Eingebettete Systeme (Handys, Autos, usw.) - Flächendeckende Verbreitung im betrieblichen Bereich Abhängigkeit von den Systemen  Systeme werden immer komplexer - Mooresches Gesetz - Betriebssystementwicklung Fehler schwieriger zu finden 4 WIRTSCHAFTS 1. Motivation INFORMATIK Fehler verursachen hohe Kosten Ariane 5 (1996) Pentium-Division (1994) Quelle: http://www.cpu-museum.de/?m=Intel&f=Pentium+P5 Die neue "Ariane 5 ESC-A" auf der Startrampe. (Foto: ESA) 5 WIRTSCHAFTS Gliederung INFORMATIK 1. Motivation 2. 2. Model ModelChecking Checking 2.1 Modellbildung 2.2 Spezifikation 2.3 Verifikation 3. Binary Decision Diagrams 4. Symbolisches Model Checking 5. Fazit 6 WIRTSCHAFTS 2. Model Checking INFORMATIK + automatisch -bei Fehlern Ausgabe eines Fehlerpfades -kein Eingriff während des Algorithmus nötig - endlicher Zustandraum -state expolsion problem 7 WIRTSCHAFTS 2.1 Modellbildung INFORMATIK Sei AP eine Menge atomarer Aussagen. Als Kripke-Struktur wird ein Tripel M = (S, R, L) über AP bezeichnet mit  S als endliche Menge von Systemzuständen,  einer totalen Transitionsmenge R ⊆ S×S, so dass jeder Zustand s ∈ S einen Nachfolger t ∈ S in der Form hat, dass gilt R(s,t),  einer Funktion L, die jedem Zustand s ∈ S eine Menge der in s wahren atomaren Aussagen zuweist. 8 WIRTSCHAFTS 2.1 Modellbildung INFORMATIK Ein Pfad mit einem Startzustand s ist eine unendliche Folge von Zuständen π = s0,s1,s2,s3,… , so dass s0 = s und R(si, si+1) für alle i ≥ 0 gilt. Beispielsweise s1,s2,s2,s5,s6,…. 9 WIRTSCHAFTS 2.1 Modellbildung INFORMATIK state explosion problem  Variable mit n Bits hat 2n Zustände.  Bei n parallelen, unabhängigen Prozessen gibt es n! unterschiedliche Ausführungsreihenfolgen. Lösungsansätze:  Symbolische Darstellung der Zustandsmenge  Partial Order Reduction 10 WIRTSCHAFTS 2.2 Spezifikation INFORMATIK Eine CTL Formel kann folgende Elemente enthalten:  Aussagevariablen (atomar): (vgl. Menge AP der Kripke-Struktur),  Boolesche Operatoren: ∧,∨,…(16 Operatoren),  Pfadquantoren: A (auf allen Pfaden gilt), E (auf mindestens einem Pfad gilt),  temporale Operatoren: X (Nachfolger), F (zukünftig), G (immer), U (bis) und R (Komplement zu U). Auf einen Pfadquantor folgt immer ein temporaler Operator und alle 10 Kombinationen lassen sich durch EX, EG und EU ausdrücken. 11 WIRTSCHAFTS 2.2 Spezifikation INFORMATIK CTL Formeln 12 WIRTSCHAFTS 2.3 Verifikation INFORMATIK 2. Model Checking 2.1 Modellbildung: Kripke-Struktur 2.2 Spezifikation: CTL Formel 2.3 2.3 Verifikation Verifikation 2.3.1 Fixpunkte 2.3.2 kleinste/größte Fixpunkte 2.3.3 CTL Model Checking Es muss ein Algorithmus definiert werden, mit dem man in der Lage ist zu prüfen, ob eine Kripke-Struktur einer CTL Formel genügt. 13 WIRTSCHAFTS 2.3.1 Fixpunkte INFORMATIK P ({s1,s2,s3}) bzgl. der Teilmengenrelation ⊆ P 14 WIRTSCHAFTS 2.3.1 Fixpunkte INFORMATIK 15 WIRTSCHAFTS 2.3.2 Kleinste / größte Fixpunkte INFORMATIK 16 WIRTSCHAFTS 2.3.2 Kleinste / größte Fixpunkte INFORMATIK 17  WIRTSCHAFTS 2.3.3 CTL Model Checking INFORMATIK function getExtremeFixpoint(τ: Funktional, Z{false,true}):Z; begin Z’ = τ(Z); while(Z’≠Z)do Z = Z’; Z’ = τ(Z); end while; return(Z); end function. 18 WIRTSCHAFTS 2.3.3 CTL Model Checking: Beispiel 1 INFORMATIK Z’= Z = τ( τ(τ( true true ) )) true EG p τ(τ(τ(true))) τ= Z = true; s1 s2 s3 p p p, Z’= τ(Z); r while(Z’≠Z)do Z = Z’; Z’ = τ(Z); end while; s4 s5 s6 p r return(Z); == ≠ Z =ZZ{s ==1{s ,s{s 1,s 2,s 1 2,s 3,s 2 3}5} 4,s 3 ,s6} 19 WIRTSCHAFTS 2.3.3 CTL Model Checking: Beispiel 2 INFORMATIK E[p U r] = 1. 2. Hallo Hallo Hallo Hallo Hallo Hallo Hallo Hallo Hallo Hallo 3. 4. Hallo Hallo Hallo Hallo Hallo Hallo Hallo Hallo Hallo Hallo 20 WIRTSCHAFTS Gliederung INFORMATIK 1. Motivation 2. Model Checking 3. 3. Binary Binary Decision Diagrams Decision Diagrams 3.1 Ordered Binary Decision Diagrams 3.2 Operationen auf OBDDs 3.3 Komplexitätsbetrachtungen 4. Symbolisches Model Checking 5. Fazit 21 WIRTSCHAFTS 3.1 Ordered Binary Decision Diagrams INFORMATIK 3. Binary Decision Diagrams 3.1 3.1 Ordered OrderedBinary BinaryDecision DecisionDiagrams Diagrams 3.1.1 Definition Binary Decision Diagrams 3.1.2 Ordnung und Reduktion 3.1.3 Problem der Variablenordnung 3.2 Operationen auf OBDDs 3.3 Komplexitätsbetrachtungen 22 WIRTSCHAFTS 3.1.1 Definition Binary Decision Diagram INFORMATIK Ein Binary Decision Diagram (BDD) stellt eine Boolesche Funktion als einen gerichteten, azyklischen Graphen dar. f  (x1  x 2 )  x 3  Alle Endknoten (Blätter) sind entweder mit 0 oder 1 markiert.  Jeder andere Knoten k repräsentiert eine binäre Variable xi und hat genau zwei Nachfolger: - lo(k), wenn xi=0 - hi(k), wenn xi=1 23 WIRTSCHAFTS 3.1.2 Ordnung und Reduktion INFORMATIK Ordered BDD (Randal E. Bryant 1986) Effiziente Darstellung von (vielen) Booleschen Funktionen durch zwei Einschränkungen auf BDDs: 1. Ordnung des BDD -> OBDD 2. Reduktion des OBDD -> (Reduced) OBDD 24 WIRTSCHAFTS 3.1.2 Ordnung und Reduktion INFORMATIK 1. Ordnung  totale Ordnung auf die Menge der Variablen, so dass für jeden Knoten k mit dem Wert xi gilt: - ∄ n ∈ {lo(k), hi(k)} mit xj, dass gilt: i,j ∈1..n und j≥i 25 WIRTSCHAFTS 3.1.2 Ordnung und Reduktion INFORMATIK 2. Reduktion (zwei Regeln) verdeckung 26 WIRTSCHAFTS 3.1.2 Ordnung und Reduktion INFORMATIK Beispiel: verdeckung verdeckung verdeckung 27 WIRTSCHAFTS 3.1.2 Ordnung und Reduktion INFORMATIK OBDD Ein Ordered Binary Decision Diagram (OBDD) stellt eine Boolesche Funktion als einen gerichteten, azyklischen Graphen dar, der sowohl geordnet als auch reduziert ist.  Genau ein Blatt hat den Wert 0, das andere den Wert 1.  Jeder andere Knoten k repräsentiert eine binäre Variable xi und hat genau zwei Nachfolger: - lo(k), wenn xi=0 - hi(k), wenn xi=1 Ein OBDD ist eine kanonische Darstellung einer Booleschen Funktion. 28 WIRTSCHAFTS 3.1.3 Problem der Variablenordnung INFORMATIK OBDDs zu derselben Funktion (a1  b1 )  (a 2  b2 )  (a 3  b3 ) a1  b1  a 2  b2  a 3  b3 a1  a 2  a 3  b1  b2  b3 29 WIRTSCHAFTS 3.1.3 Problem der Variablenordnung INFORMATIK Sifting-Algorithmus // Phase 1: Ermittlung der lokal besten Position von x2 x1 x2 x3 x4 x1 Rekursion beendet 2. F und/oder G sind keine Blätter -> rekursiver Aufruf von Apply 2.1 Startknoten beider OBDD repräsentieren die gleiche Variable 2.2 Startknoten repräsentieren nicht die gleiche Variable 34 WIRTSCHAFTS 3.2.2 Apply INFORMATIK 2.1: Beide Startknoten repräsentieren x1  Knoten mit x1 wird erzeugt.  Zwei rekursive Aufrufe von Apply. 35 WIRTSCHAFTS 3.2.2 Apply INFORMATIK 2.2: F repräsentiert die „kleinere Variable“ x2  Knoten mit x2 wird erzeugt.  Zwei rekursive Aufrufe von Apply. 36 WIRTSCHAFTS 3.2.2 Apply INFORMATIK 2.2: G repräsentiert die „kleinere Variable“ x3  Knoten mit x3 wird erzeugt.  Zwei rekursive Aufrufe von Apply. 37 WIRTSCHAFTS 3.2.2 Apply INFORMATIK 1: F und G sind Blätter  Ein Blatt wird entsprechend dem Booleschen Operator erzeugt.  Apply wird mehr rekursiv aufgerufen. 38 WIRTSCHAFTS 3.2.2 Apply INFORMATIK 1: F und G sind Blätter  Ein Blatt wird entsprechend dem Booleschen Operator erzeugt.  Apply wird mehr rekursiv aufgerufen. 39 WIRTSCHAFTS 3.2.2 Apply INFORMATIK 2.1: Beide Startknoten repräsentieren x3  Knoten mit x3 wird erzeugt.  Zwei rekursive Aufrufe von Apply. 40 WIRTSCHAFTS 3.2.2 Apply INFORMATIK 1: F und G sind Blätter  Es wird auf ein bereits berechnetes Ergebnis zurückgegriffen.  Kein rekursiver Aufruf von Apply. 41 WIRTSCHAFTS 3.2.2 Apply INFORMATIK 1: F und G sind Blätter  Ein Blatt wird entsprechend dem Booleschen Operator erzeugt.  Kein rekursiver Aufruf von Apply. 42 WIRTSCHAFTS 3.2.2 Apply INFORMATIK 2.2: F repräsentiert die „kleinere Variable“ x3  Ein Blatt wird entsprechend dem Booleschen Operator erzeugt.  Apply ist fertig. Das Ergebnis-OBDD ist nicht reduziert. 43 WIRTSCHAFTS 3.2.2 Apply INFORMATIK Komplexität von Apply: O(|F|*|G|) Tricks: 1. Frühzeitige Auswertung 2. Hashtabelle zum Speichern der Berechnungen 44 WIRTSCHAFTS 3.2.3 AndExists INFORMATIK existentielle Quantifizierung von Variablen  Für eine Boolesche Funktion ist die existenzielle Quantifizierung bezüglich der Variablen x definiert durch x.f  f x 0  f x 1  Für einen Vektor x  (x1 ,..., x n ) gilt: x.f  V (x.f )(a) a{false,true}n 45 WIRTSCHAFTS 3.2.3 AndExists INFORMATIK AndExists funktioniert wie Apply mit der Konjunktion (∧) als Booleschen Operator. Die einzige Änderung ist: x.f  f x 0  f x 1 46 WIRTSCHAFTS 3.2.3 AndExists – Beispiel INFORMATIK 47 WIRTSCHAFTS 3.2.3 AndExists – Beispiel INFORMATIK 48 WIRTSCHAFTS 3.2.3 AndExists – Beispiel INFORMATIK 49 WIRTSCHAFTS 3.2.3 AndExists – Beispiel INFORMATIK 50 WIRTSCHAFTS 3.2.3 AndExists – Beispiel INFORMATIK 51 WIRTSCHAFTS 3.2.3 AndExists – Beispiel INFORMATIK Das Ergebnis von AndExists ist nicht reduziert. 52 WIRTSCHAFTS 3.2.3 AndExists – Beispiel INFORMATIK 53 WIRTSCHAFTS 3.2.3 AndExists – Beispiel INFORMATIK 54 WIRTSCHAFTS 3.3 Komplexitätsbetrachtungen INFORMATIK 3. Binary Decision Diagrams 3.1 Ordered Binary Decision Diagrams 3.2 Operationen auf OBDDs 3.3 3.3 Komplexitätsbetrachtungen Komplexitätsbetrachtungen 3.3.1 Darstellung Boolescher Funktionen als OBDDs 3.3.2 Operationen auf OBDDs 55 3.3.1 Darstellung Boolescher WIRTSCHAFTS INFORMATIK Funktionen als OBDDs Funktionsklasse Komplexität bester Fall schlechtester Fall symmetrisch linear quadratisch Integer Addition linear exponentiell Integer Multiplikation exponentiell exponentiell 56 WIRTSCHAFTS 3.3.2 Operationen auf OBDDs INFORMATIK Algorithmus Komplexität Reduktion von F proportional zur Knotenanzahl: O(F) Variablenordnung mit Sifting O(n2) Vertauschungen zweier Variablen Negation konstant (Vertauschung der Blätter) Apply(F,G,*) quadratisch: O(|F|*|G|) AndExists((x1,…,xn),F,G) exponentiell: O(|F|*|G|*22n) 57 WIRTSCHAFTS Gliederung INFORMATIK 1. Motivation 2. Model Checking 3. Binary Decision Diagrams 4. Symbolisches Model 4. Symbolisches Checking Model Checking 4.1 Modellbildung 4.2 Spezifikation 4.3 Verifikation 5. Fazit 58 WIRTSCHAFTS 4.1 Modellbildung INFORMATIK Symbolische Darstellung der Kripke-Struktur 59 WIRTSCHAFTS 4.1 Modellbildung INFORMATIK M = (S, S0, R, L)  Ein Zustand kann durch einen Vektor Boolescher Werte ausgedrückt werden: z.B. s1 ≙ (0,0)  Eine Menge von Zuständen kann eindeutig durch ein Funktional dargestellt werden: p  (x1 ,..., x n ).p - OBDD p enthält nur die Variablen x1,…,xn - p ist eine Menge von Booleschen Vektoren 60 WIRTSCHAFTS 4.1 Modellbildung INFORMATIK M = (S, S0, R, L)  Beispiel zur Menge von Zuständen: p  (x1 ,..., x n ).p Boolescher Vektor (x2, x1): s3 und s4: (x 2  x1 )  (x 2  x1 )  x 2 = p  (1) ≙ Menge der Zustände, in denen r∈AP gilt. 61 WIRTSCHAFTS 4.1 Modellbildung INFORMATIK M = (S, S0, R, L)  Ein Zustandsübergang wird durch ein Paar von Zuständen ausgedrückt: (s,s) z.B. (s1,s2)≙( (0,0), (0,1) )  Eine Menge von Zustandsübergängen kann eindeutig durch ein Funktional dargestellt werden: R  ((x1 ,..., x n ),(x1 ,..., x n )). R - OBDD R enthält nur die Variablen x1,…, xn, x1´,…, xn´ - R ist eine Menge von Paaren Boolescher Vektoren 62 WIRTSCHAFTS 4.1 Modellbildung INFORMATIK M = (S, S0, R, L) R  ((x1 ,..., x n ),(x1 ,..., x n )). R Überlagerung R = ((s 1,s2), (s2,s2), (s2,s3), (s3,s4)) ≙ 63 WIRTSCHAFTS 4.1 Modellbildung INFORMATIK M = (S, S0, R, L)  Anhand einer atomaren Aussage wird ein OBDD mit denjenigen Zuständen zurückgegeben, in denen die Aussage gilt. L(p) = (x 2  x1 )  (x 2  x1 )  (x 2  x1 )  x 2  (x 2  x1 ) 64 WIRTSCHAFTS 4.2 Spezifikation INFORMATIK Zur Erinnerung: 65 WIRTSCHAFTS 4.2 Spezifikation INFORMATIK Gesucht: CTL-Operator EX auf symbolischer Kripke-Struktur Gegeben: EXp ≙ (x1 ,..., x n )  x Nachfolger (x1 ,..., xn )  x Übergang ((x1 ,..., x n ),(x1 ,..., x n )) Lösung: 66 WIRTSCHAFTS 4.2 Spezifikation INFORMATIK EXp  x.x .(R(x, x )  p(x )) R  ((x1 ,..., x n ),(x1 ,..., x n )).R p  (x1 ,..., x n ).p EXp  x.x.(R  p) AndExists Algorithmus 67 WIRTSCHAFTS 4.3 Verifikation INFORMATIK Analyse der Formel AndExists kleinster Fixpunkt größter Fixpunkt 68 WIRTSCHAFTS 4.3 Verifikation: Beispiel INFORMATIK EG p 69 WIRTSCHAFTS 4.3 Verifikation: Beispiel INFORMATIK 70 WIRTSCHAFTS 4.3 Verifikation: Beispiel INFORMATIK 71 WIRTSCHAFTS 4.3 Verifikation: Beispiel INFORMATIK 72 WIRTSCHAFTS 4.3 Verifikation: Beispiel INFORMATIK 73 WIRTSCHAFTS 4.3 Verifikation: Beispiel INFORMATIK 74 WIRTSCHAFTS 4.3 Verifikation: Beispiel INFORMATIK 75 WIRTSCHAFTS Gliederung INFORMATIK 1. Motivation 2. Model Checking 3. Binary Decision Diagrams 4. Symbolisches Model Checking 5. Fazit 5. Fazit 76 WIRTSCHAFTS 5. Fazit INFORMATIK  Der vorgestellte Algorithmus zum Symbolischen Model Checking ist ein effizientes Verfahren zur automatischen Verifikation.  Grenzen des Model Checking: - endlicher Zustandsraum - state explosion problem  Symbolic Model Verifier (SMV) System in der Praxis - Cache-Protokoll im IEEE-Futurebus+ (1992)  bisherige Erfolge vor allem im Hardwarebereich und bei Kommunikationsprotokollen 77 WIRTSCHAFTS 5. Fazit INFORMATIK  große Unternehmen aktiv im Bereich Model Checking - SLAM Projekt von Microsoft: Treiberverifikation bei Windows XP  aktuelle Forschungsrichtung: Software Model Checking  Verbesserungen notwendig - einheitlicher Ansatz mit deduktiver Verifikation 78 WIRTSCHAFTS INFORMATIK Vielen Dank für die Aufmerksamkeit! 79
Related Search
We Need Your Support
Thank you for visiting our website and your interest in our free products and services. We are nonprofit website to share and download documents. To the running of this website, we need your help to support us.

Thanks to everyone for your continued support.

No, Thanks