Formale Spezifikation und Verifikation

Formal = Mittels Logik

• $\bigwedge \emptyset = \top$
• $\bigvee \emptyset = \perp$

Nur erfüllungsäquivalent

• Rekursive Funktion KNF
  • Rein
    • (Nicht-Normalisierte) Formel
  • Raus
    • Neuster (frischer) Variablenname
    • KNF
• C ist frische Variable
• Regel: $C \Leftrightarrow \phi$ als KNF
  1. Tabelle Erstellen
  2. Bei 0: Veroderung (Disjunktion) erstellen ($A=0 \Rightarrow A$ / $A=1 \Rightarrow \neg A$)
  3. Verodrungen verunden (Konjunktion)

SAT

• “ist $\phi$ erfüllbar?”
• Entscheidungsproblem (NP-Hart)
• Nur für KNF

• Erweiterung auf nicht KNF: Tseitin Übersetzung
• Erweiterung auf Äquivalenz von $\phi$ und $\psi$: $\neg (\phi \Leftrightarrow \psi)$ unerfüllbar?

• Rekursive Funktion DPLL
  • Rein
    • (Teil) Besetzung
    • (Rest) KNF
  • Raus
    • Bessere Belegung

Wenn gezeigt werden soll, das die Schaltungen $f$ und $f'$ bezüglich ihrer Eingänge $x\ldots$ das selbe liefern, dann darf $\neg \left( \left(f_1(x\ldots) \Leftrightarrow f'_1(x\ldots)\right) \wedge \left(f_2(x\ldots) \Leftrightarrow f'_2(x\ldots)\right)\right)$ keine Lösung liefern.

Dieses System darf keine Lösung haben.

nichtreduzierter BDDs

• Gerichtet
• Azyklisch
• Knoten auf Pfad mit fixer Ordnung (es dürfen welche fehlen)

reduzierte BDDs (zusätzlich)

• Keine Kanten mit identischen Start und Ziel (gleich ist OK)
• Keine Redundanz (isomarphen Teilgraphen)
• Nur True und False als Blätter (jeweils max. 1x)

nichtreduziert → reduziert

• Knoten mit identischen Nachfolgern entfernen
• Knoten: Name gleich & Nachfolger gleich ⇒ verschmelzen
• True/False verschmelzen.

BDDs sind eindeutig: Gleiche Funktion ⇒ isomorphe BDDs

Shannon-Zerlegung: $f = (x \wedge f[x := \top]) \vee (\neg x \wedge f[x := \perp])$

Negation: True und False vertauschen

Variable setzen:

1. ersetzen/umlenken
2. reduzieren

Zweistellige Operationen: Rekursiv $(x \wedge (f[x := \top] \oplus g[x := \top])) \vee (\neg x (\wedge f[X := \perp] \oplus g[x := \perp]))$ (Gehe die Variablen der reihe nach durch. Ersetze die Nachfolger durch $\oplus$ aus den True-Zweigen und durch $\oplus$ aus den False-Zweigen.)

Alle möglichkeiten einer Variablen probieren: $\exists x: f := f[x := \top] \vee f[x :=\perp]$

Optiomierungen

• Umordnen (extremfall: explonential)
• Teilographen wiederverwenden (Hash-Funktion zum finden)

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

$AG \Leftrightarrow \neg EF(\neg \phi)$

$(S, \rightarrow)$

• Zustandsmenge: $\{(False, True), (True, False), (True, True)\}$
• Transitionsrealtion: $\{\left(\left(Fals, True\right), \left(True, False\right)\right), \ldots\}$

Interpretation enthält keine Formel.

• (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))$

1. Formel umformen (nur noch $\neg, \wedge, \perp, AF, E[\cdot U \cdot ]$)
2. Teilformeln bis auf Variablen-Ebene finden
3. Teilformeln Bottom-up durchgehen, bis nichts mehr geht
   1. 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)$

1. $\neg\phi$ für Ausblenden/Ignorieren/Streichen
2. Starke Zusammenhangskomponenten markieren (Ring-Pfad durch Knoten)
3. 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)

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

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

• Fairness direkt angebbar: (GF p1.state=running) ⇒ …
• CTL ist ausdrucksstärker
• Für alle Pfade muss … gelten

$(\Sigma, T, I, E, \delta)$

• 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)

• while […] do …
• if […] then … else …
• true
• false
• not …
• … := …
• Aritmetische Ausdrücke
• Boolsche Ausdrücke

“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.

So lange ausfüllen, bis nichts mehr geht.

Das geht, weil Fixpunkte und Knaster-Tarski-Theorem

Teile

1. MODULE
2. VAR
3. ASSIGN
4. INIT
5. TRANS
6. SPEC
7. 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 main

– oder –

MODULE p(x, y, z)

• Keine Typ angaben

VAR
  a : boolean;
  b : {foo, bar};
  c : process otherModule(foo, bar);

• … : … ;
• boolean
• Set: {}

ASSIGN
  init(b) := foo;
  next(b) := {foo, bar};
  next(b) := case
               foo  : bar;
               TRUE : {foo, bar};
             esac;
  c := !b

• … := …;
• init()
• next()
• Invarianten
• case … esac
• Ersetzt INIT, TRANS und INVAR

Bei case: Boolscher Test: Wert/Set;

INIT
  b = foo;

• … = … ;

TRANS
    b = foo & next(b) = bar
  | b = bar & next(b) = foo
  | b = bar & next(b) = bar

• Transition, wenn Formel erfüllt

INVAR
  Ziege.pos = Wolf.pos -> Bauer.pos = Ziege.pos

• Invariante

SPEC
  AG(a -> AF b = foo)

DEFINE
  foo := myVar = foo & myOtherVAr = bar;

• … := … ;

JUSTICE/FAIRNESS
  p1.status = running

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$

$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'$

• $x \sqsubseteq y \Rightarrow F(x) \sqsubseteq F(y)$

• $\exists x: F(x) = x$

Dazu muss $F(x)$ monoton sein.

• Zwei Kommunikationspartner
• Bidirektionaler Kanal
• Nachricht: OK/Defekt
• So lange wiederholen bis es klapt

OK

Fehler