Wiki

A universe of ideas

User Tools

Site Tools

You are here: A universe of ideas » Uni » 6. Semester » Formale Spezifikation und Verifikation
Trace:
uni:6:fsv:start

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revisionPrevious revision
Next revision		Previous revision
uni:6:fsv:start [2014-07-11 00:43] – [Tseitin Übersetzung] skrupellosuni:6:fsv:start [2020-11-18 18:11] (current) – external edit 127.0.0.1
Line 131: Line 131:
   * Umordnen (extremfall: explonential)   * Umordnen (extremfall: explonential)
   * Teilographen wiederverwenden (Hash-Funktion zum finden)   * Teilographen wiederverwenden (Hash-Funktion zum finden)
 +
 +<WRAP center round important 60%>
 +Es fehlen nebenläufige Systeme!!!
 +</WRAP>
 +
 +===== Model checking =====
 +Arten
 +  * Bounded (Beschränkt durch die Symulationszeit)
 +    * SAT Solver
 +  * Symbolic
 +    * BDDs
 +
 +Dinge die Interessieren
 +  * Safty: Keine verbotenen Zustände erreichbar
 +  * Liveness: Reset-Zustand immer erreichbar? Kein verklemmen $AG(EF\bigwedge_p q_{p,sleep})$
 +  * Fairness: "Gute Eigenschaft" gilt für alle fairen Abläufe
 +
 +==== CTL ====
 +
 +^ Propositionale Variablen | $p, q, \ldots$ | Jedes Aussgenlogische Formel ist CTL! |
 +^ Junktoren | $\neg, \wedge, \vee, \Rightarrow, \Leftrightarrow$ | ::: |
 +^ Formel | $\phi, \psi, \ldots$ | ::: |
 +^ Konstanten | $\top, \perp$ | ::: |
 +^ Foo | $AX, EX, A[\phi U \psi], E[\phi U \psi], AG \phi, AF \phi, EG \phi, EF \phi$ | |
 +
 +
 +$AG \Leftrightarrow \neg EF(\neg \phi)$
 +<WRAP second column>
 +^A|Auf allen Pfaden gilt ...|
 +^E|Auf (mindestens) einem Pfad gilt ...|
 +</WRAP>
 +<WRAP second column>
 +...in...
 +</WRAP>
 +<WRAP second column>
 +^X|Ne**x**t|... (mindestens) einem unmittelbar folgenden Zustand|
 +^F|**F**inal|... (mindestens) einem folgenden/selben Zustand|
 +^G|**G**lobaly|... allen folgenden/selben Zuständen|
 +^U|**U**ntil|... allen folgenden/selben Zuständen $\phi$, bis $\psi$ gilt. \\ $\psi$ kann bereits im selben gelten|
 +</WRAP>
 +
 +=== Transitinssystem ===
 +$(S, \rightarrow)$
 +
 +  * Zustands//menge//: $\{(False, True), (True, False), (True, True)\}$
 +  * Transitionsrealtion: $\{\left(\left(Fals, True\right), \left(True, False\right)\right), \ldots\}$
 +
 +===Interpretationen===
 +^ $Tr(\mathcal{I})$ | $(S, \rightarrow)$ | Transitionsystem | Durch $\mathcal{I}$ festgelegt |
 +^ $\mathcal{I}(p)$  | $\subseteq S$ | Zustände in denen $p$ gilt | ::: |
 +^ $s \models \mathcal{I} p$ | $\{True, False\}$ | Aussage: $p$ ist in Zustand $s$ gesetzt | ::: |
 +^ $\mathcal{I}(\phi)$  | $\subseteq S$ | Zustände in denen $\phi$ gilt | Ableitbar |
 +^ $s \models \mathcal{I} \phi$ | $\{True, False\}$ | Aussage: $\phi$ ist in Zustand $s$ gesetzt | ::: |
 +
 +Interpretation enthält keine Formel.
 +
 +===Äquivalenz ===
 +  * (AE)(GF) vertauschen und 2xnegieren
 +    * $AG(\phi) \Longleftrightarrow \neg EF(\neg \phi)$
 +    * $AF(\phi) \Longleftrightarrow \neg EG(\neg \phi)$
 +    * $EF(\phi) \Longleftrightarrow \neg AG(\neg \phi)$
 +    * $EG(\phi) \Longleftrightarrow \neg AF(\neg \phi)$
 +  * $AG(\phi \wedge \psi) \Longleftrightarrow AG(\phi) \wedge AG(\psi)$
 +  * $AF(\phi) \Longleftrightarrow A[\top U \phi]$
 +  * $EF(\phi) \Longleftrightarrow E[\top U \phi]$
 +  * $A\[\phi U \psi\] \Longleftrightarrow \neg (E[\neg \phi U (\neg \phi \wedge \neg \psi)] \vee EG(\neg \phi))$
 +
 +=== Labeling Algorithmus ===
 +  - Formel umformen (nur noch $\neg, \wedge, \perp, AF, E[\cdot U \cdot ]$)
 +  - Teilformeln bis auf Variablen-Ebene finden
 +  - Teilformeln Bottom-up durchgehen, bis nichts mehr geht
 +    - Graph mit geltenden Teilformeln markieren, bis nichts mehr geht (dabei auf bereits markiertes berufen)
 +
 +Markiere mit ..
 +  * $AF(\phi)$, wo ..
 +    * $\phi$
 +    * Alle Nachfolger sind $AF(\phi)$
 +  * $E[\phi U \psi]$, wo ..
 +    * $\psi$
 +    * $\phi$ und Folgezustand mit $E[\phi U \psi]$
 +
 +Effizienter: $EG(\phi)$ anstatt $AF(\phi)$
 +  - $\neg\phi$ für Ausblenden/Ignorieren/Streichen
 +  - Starke Zusammenhangskomponenten markieren (Ring-Pfad durch Knoten)
 +  - Markiere Knoten, die in eine  //echte// starke Zusammenhangskomponenten zeigen
 +
 +Zeitkomplexität: Linear zu Transitionen
 +
 +Aber //state-explosion-problem//: Exponentiell mit Anzahl zu modelierender Prozesse \\ => BDDs verhindern das (es kann optimiert werden)
 +
 +=== Fairnes ===
 +Alle interessierenden Zustände können immer unendlich offt erreicht werden.
 +
 +  * D.h. für ''E?'', es Existiert ein fairer Pfad in dem ...
 +  * D.h. für ''A?'', in allen fairen Pfaden gild ...
 +
 +Abwandlung des Labeling Algorithmuses:
 +  * Starke Zusammenhangskomponente ist fair, wenn ein Zustand Fairnesbedingung erfüllt
 +  * Zustand ist fair, wenn ein (längerer) Pfad zu fairen starken Zusamenhangskomponente existiert
 +
 +=== Encoding of CTL in BDD ===
 +BDD ist ein Bitvektor und daher kann ich ein Transitionsystem eincodieren, sowie ein $\phi$.
 +
 +http://nicta.com.au/__data/assets/pdf_file/0018/14814/lecture4-mc2.pdf
 +
 +<WRAP center round important 60%>
 +ToDo
 +</WRAP>
 +
 +==== LTL ====
 +^ Propositionale Variablen | $p, q, \ldots$ | **eingeschränktes** CTL! |
 +^ Junktoren | $\neg, \wedge$ | ::: |
 +^ Formel | $\phi, \psi, \ldots$ | ::: |
 +^ Konstanten | $\top$ | ::: |
 +^ Foo | $X \phi, F \phi, G \phi, \phi U \psi$ | |
 +
 +  * Fairness direkt angebbar: ''**(GF** p1.state=running**) =>** ...''
 +  * CTL ist ausdrucksstärker
 +  * Für **alle** Pfade muss ... gelten
 +
 +==== Büchi Automat ====
 +$(\Sigma, T, I, E, \delta)$
 +
 +| $\Sigma$ | Menge | Alphabet |
 +| $Z$ | Menge | Zustände |
 +| $I$ | Menge | Anfangszustände |
 +| $E$ | Menge | Endzustände |
 +| $\delta$ | Relation | Zustandsübergänge |
 +
 +  * Nichtdeterministisch
 +  * Unendliche Wörter
 +  * Akzeptiert: Wenn mindestens ein Lauf //existiert//, der immer zu einem Endzustand kommen (unendlich offt)
 +
 +$L = (b^{*}a)^\omega$ (wenn ''a'' immer wieder vorkommen muss)
 +
 +| $\omega$ | FG | Unendlich offt vorkommen |
 +| $*$      | GF | Endlich offt vorkommen   |
 +
 +===== Typanalyse =====
 +==== While Programm ====
 +  * ''**while [**...**] do **...''
 +  * ''**if [**...**] then **...** else **...''
 +  * ''**true**''
 +  * ''**false**''
 +  * ''**not **...''
 +  * ''... **:= **...''
 +  * Aritmetische Ausdrücke
 +  * Boolsche Ausdrücke
 +
 +==== Datenflussgleichung ====
 +"Erreichbare Definitionen" (Reachable Definitions)
 +
 +  * $RD_{{\color{ForestGreen}entry}}(\ell) = \bigcup_{{\color{red}\ell'}:{\color{red}\ell'}\rightarrow\ell}RD_{exit}({\color{red}\ell'})$
 +  * $RD_{exit}(\ell) = (RD_{{\color{ForestGreen}entry}}(\ell) \setminus \text{"Entwertete Zuweisungen"}) \cup \text{ "Neue Zuweisungen"}$
 +  * Zu beginn werden //alle// Variablen mit "$(X, \ell)$" initialisiert.
 +
 +
 +
 +"Verfügbare Ausdrücke" (Available Expressions)
 +  * $AE_{{\color{ForestGreen}entry}}(\ell) = {\color{blue}\bigcap}_{{\color{red}\ell'}:{\color{red}\ell'}\rightarrow\ell}AE_{exit}({\color{red}\ell'})$
 +  * $AE_{exit}(\ell) = (AE_{{\color{ForestGreen}entry}}(\ell) \setminus kill_{AE}(B^\ell)) \cup gen_{AE}(B^\ell)$
 +  * $kill_{AE}([x:=a]^\ell) = \{\text{Formeln, die }x\text{ enthalten}\}$
 +  * $gen_{AE}([x := a]) = \{\text{Teilausdrücke von }a\text{ ohne }x\}$
 +  * $gen_{AE}([bool\ exp]) = \{\text{Teilausdrücke von }bool\ exp\}$
 +  * Zu beginn werden //alle// Variablen mit "$\emptyset$" initialisiert.
 +  * //Nur// Arithmetische Ausdrücke
 +
 +
 +"Lebendige Variablen" (Live Variables)
 +  * $LV_{exit}(\ell) = \bigcup_{{\color{red}\ell'}:\ell\rightarrow{\color{red}\ell'}}LV_{{\color{ForestGreen}entry}}({\color{red}\ell'})$
 +  * $LV_{{\color{ForestGreen}entry}}(\ell) = (LV_{exit}(\ell) \setminus kill_{LV}(B^\ell)) \cup gen_{LV}(B^\ell)$
 +  * $kill_{LV}([x:=a]^\ell) = \{x\}$
 +  * $gen_{LV}([x := a]) = \{\text{Variablen in }a\}$
 +  * $gen_{LV}([bool\ exp]) = \{\text{Variablen in }bool\ exp\}$
 +  * Zu beginn werden //alle// Variablen mit "$\emptyset$" initialisiert.
 +
 +^ $\ell$ ^ $RD_{entry}(\ell)$ ^ $RD_{exit}(\ell)$ ^
 +| 1 | (x, ?), (y, ?) | ... |
 +| 2 | ... | ... |
 +| 3 | ... | ... |
 +
 +So lange ausfüllen, bis nichts mehr geht.
 +
 +Das geht, weil //Fixpunkte// und //Knaster-Tarski-Theorem//
 +==== SMV ====
 +Teile
 +  - MODULE
 +  - VAR
 +  - ASSIGN
 +  - INIT
 +  - TRANS
 +  - SPEC
 +  - JUSTICE/FAIRNESS
 +
 +  * Case sensitive
 +  * Wenn uterspezifiziert: Deterministisch
 +  * Wenn Block mehrfach: Konjunktion
 +  * Nur einzelnes Zeichen: **''&''** bzw. **''|''**
 +  * Nur Einfacher Strich: **''%%->%%''** für =>
 +  * Negieren, um Lösung als Gegenbeispiel zu bekommen
 +
 +=== MODULE ===
 +<code>
 +MODULE main
 +</code>
 +-- oder --
 +<code>
 +MODULE p(x, y, z)
 +</code>
 +  * Keine Typ angaben
 +
 +=== VAR ===
 +<code>
 +VAR
 +  a : boolean;
 +  b : {foo, bar};
 +  c : process otherModule(foo, bar);
 +</code>
 +  * ''... **:** ... **;**''
 +  * ''boolean''
 +  * Set: ''{}''
 +
 +=== ASSIGN ===
 +<code>
 +ASSIGN
 +  init(b) := foo;
 +  next(b) := {foo, bar};
 +  next(b) := case
 +               foo  : bar;
 +               TRUE : {foo, bar};
 +             esac;
 +  c := !b
 +</code>
 +  * ''... **:=** ...**;**''
 +  * ''init()''
 +  * ''next()''
 +  * Invarianten
 +  * ''case ... esac''
 +  * Ersetzt ''INIT'', ''TRANS'' und ''INVAR''
 +
 +Bei ''case'': ''Boolscher Test: Wert/Set;''
 +
 +=== INIT ===
 +<code>
 +INIT
 +  b = foo;
 +</code>
 +  * ''... **=** ... **;**''
 +
 +=== TRANS ===
 +<code>
 +TRANS
 +    b = foo & next(b) = bar
 +  | b = bar & next(b) = foo
 +  | b = bar & next(b) = bar
 +</code>
 +
 +  * Transition, wenn Formel erfüllt
 +
 +=== INVAR ===
 +<code>
 +INVAR
 +  Ziege.pos = Wolf.pos -> Bauer.pos = Ziege.pos
 +</code>
 +  * Invariante
 +
 +=== SPEC ===
 +<code>
 +SPEC
 +  AG(a -> AF b = foo)
 +</code>
 +
 +=== DEFINE ===
 +<code>
 +DEFINE
 +  foo := myVar = foo & myOtherVAr = bar;
 +</code>
 +
 +  * ''... **:=** ... **;**''
 +=== JUSTICE/FAIRNESS ===
 +<code>
 +JUSTICE/FAIRNESS
 +  p1.status = running
 +</code>
 +
 +===== Beweise =====
 +==== Vollständiger Verband ====
 +Verband $(L, \sqsubseteq)$
 +  * **reflexiv** \\ $\forall_{x \in L} : x \sqsubseteq x$
 +  * **transitiv** \\ $\forall_{x, y, z \in L} : x \sqsubseteq y \wedge y \sqsubseteq z \Rightarrow x \sqsubseteq z$
 +  * **antisymetrisch** \\ $\forall_{x, y \in L} : x \sqsubseteq y \wedge y \sqsubseteq x \Rightarrow x = y$
 +  * **Jede Teilmenge hat ein Supremum** \\ Jedes $U \subseteq L$ hat ein $\bigsqcup U$
 +
 +==== Supremum ====
 +$s = \bigsqcup U$
 +
 +  * **Ist obere Schranke** \\ $\forall_{x \in U} : x \sqsubseteq s$
 +  * **Ist //kleinste// obere Schranke** \\ $s' \text{ ist obere Schranke } \Rightarrow s \sqsubseteq s'$
 +
 +==== Monotonie ====
 +  * $x \sqsubseteq y \Rightarrow F(x) \sqsubseteq F(y)$
 + 
 +==== Fixpunkt ====
 +  * $\exists x: F(x) = x$
 +
 +Dazu muss $F(x)$ monoton sein.
 +===== Probleme =====
 +==== Semaphor ====
 +==== Alternating Bit Protocol ====
 +  * Zwei Kommunikationspartner
 +  * Bidirektionaler Kanal
 +  * Nachricht: OK/Defekt
 +  * So lange wiederholen bis es klapt
 +
 +OK
 +^ Kontrollbit: 0 ^ Nachricht | -> ^  | OK |
 +^ || <- ^ 0 | ::: |
 +^ Kontrollbit: 1 ^ Nachricht | -> ^  | OK |
 +^ || <- ^ 1 | ::: |
 +
 +Fehler
 +^ Kontrollbit: 0 ^ Nachricht | -> ^ ✘ | Fehler beim Empfänger \\ => Unerwartetes Kontrollbit zurück senden |
 +^ || <- ^ 1 | ::: |
 +^ Kontrollbit: 0 ^ Nachricht | -> ^  | Fehler beim Sender |
 +^ ✘ || <- ^ 0 | ::: |
 +^ Kontrollbit: 0 ^ Nachricht | -> ^  | OK |
 +^ || <- ^ 0 | ::: |
 +^ Kontrollbit: 1 ^ Nachricht | -> ^ ✘ | Fehler beim Empfänger \\ => Unerwartetes Kontrollbit zurück senden |
 +^ || <- ^ 0 | ::: |
 +^ Kontrollbit: 1 ^ Nachricht | -> ^  | Fehler beim Sender |
 +^ ✘ || <- ^ 1 | ::: |
 +^ Kontrollbit: 1 ^ Nachricht | -> ^  | OK |
 +^ || <- ^ 1 | ::: |
uni/6/fsv/start.1405032203.txt.gz · Last modified: (external edit)