Formale Spezifikation und Verifikation

Formal = Mittels Logik

Propositionallogik

Syntax

Propositionale Variablen	$A, B, C, \ldots$
Junktoren	$\neg, \wedge, \vee, \Rightarrow, \Leftrightarrow$
Formel	$\phi, \psi, \ldots$
Konstanten	$\top, \perp$

Semantik

Belegung	$\eta$
Foo	$⟦\phi⟧\eta$
Bar	$\&, \mid\mid$

Tautologie	$\forall \eta:⟦\phi⟧\eta$
Erfüllbar	$\exists \eta:⟦\phi⟧\eta$
Unerfüllbar	$\forall \eta:\neg⟦\phi⟧\eta$
Äquivalent	$\forall \eta:⟦\phi⟧\eta = ⟦\psi⟧\eta$
Erfüllbarkeitsäuivalenz	$(\phi \text{ und } \psi \text{ sind erfüllbar}) \vee (\phi \text{ und } \psi \text{ sind unerfüllbar})$

Normierung

Literal	$A$ und $\neg A$
Minterm	Konjunktion: $\ldots \wedge \ldots \wedge \ldots \wedge \ldots$ (Die wenigsten Belegungen sind $\top$ )
Maxterm / Klausel	Disjunktion: $\ldots \vee \ldots \vee \ldots \vee \ldots$ (Die meisten Belegungen sind $\top$ )
KNF	$(\ldots \vee \ldots \vee \ldots \vee \ldots ) \wedge ( \ldots \vee \ldots \vee \ldots \vee \ldots )$
DNF	$(\ldots \wedge \ldots \wedge \ldots \wedge \ldots) \vee (\ldots \wedge \ldots \wedge \ldots \wedge \ldots)$

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

$\phi$ … KNF	Größe	Zeit
Äquivalent	exponentiell	?
Erfüllungsäuivalent	linear	polynomiell

Tseitin Übersetzung

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)

$KNF(A) = (A, \top)$

$\begin{array}{ll}KNF(\neg\phi) =&\text{let } (B, \Gamma) = KNF(\phi) \text{ in} \\ & (C, \Gamma \wedge (C \vee B) \wedge (\neg C \vee \neg B))\end{array}$

$\begin{array}{ll}KNF(\phi_1\vee\phi_2) =&\text{let } (B_1, \Gamma_1) = KNF(\phi_1) \text{ in} \\ &\text{let } (B_2, \Gamma_2) = KNF(\phi_2) \text{ in} \\ & (C, \Gamma_1 \wedge \Gamma_2 \wedge (\neg C \vee B_1 \vee B_2) \wedge (C \vee \neg B_1) \wedge (C \vee \neg B_2))\end{array}$

SAT-Solver

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?

DPLL-Algorithmus

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

Hier gibt es mehr. Aber das halte ich für Klausurirrelevant

Gleichheit von Schaltkreisen

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.

Nebenläufige Systeme

		Zeit
		0	1	…	n-1
Zustand	$z_1$	$x_{zt}$
	$z_2$
	…

$\bigwedge_t \bigwedge_{z \in Z} \bigwedge_{z' \ne z}\neg(x_{zt} \wedge x_{z't})$	Zu jeder Zeit ist nur ein zustand gesetzt
$\bigvee_{z \in I} x_{z0}$	Einer der Startzustände
$\bigwedge^{n-2}_{t=0} \bigvee_{z \rightarrow z'} x_{zt} \wedge x_{z'(t+1)}$	Zu jeder Zeit führt ein Zustand in einen Folgezustand
$\bigvee^{n-1}_{t=0} \bigvee_{z \in V} x_{zt}$	Zu einer Zeit ist ein verbotener Zustand erreicht

Dieses System darf keine Lösung haben.

BDD

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:

ersetzen/umlenken
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)

Es fehlen nebenläufige Systeme!!!

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

A	Auf allen Pfaden gilt …
E	Auf (mindestens) einem Pfad gilt …

…in…

X	Next	… (mindestens) einem unmittelbar folgenden Zustand
F	Final	… (mindestens) einem folgenden/selben Zustand
G	Globaly	… allen folgenden/selben Zuständen
U	Until	… allen folgenden/selben Zuständen $\phi$ , bis $\psi$ gilt. $\psi$ kann bereits im selben gelten

Transitinssystem

$(S, \rightarrow)$

Zustandsmenge: $\{(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	Ableitbar

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

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

ToDo

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

MODULE main

– oder –

MODULE p(x, y, z)

Keine Typ angaben

VAR

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

… : … ;
boolean
Set: {}

ASSIGN

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

INIT
  b = foo;

… = … ;

TRANS

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

Transition, wenn Formel erfüllt

INVAR

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

Invariante

SPEC

SPEC
  AG(a -> AF b = foo)

DEFINE

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

… := … ;

JUSTICE/FAIRNESS

JUSTICE/FAIRNESS
  p1.status = running

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	OK
Kontrollbit: 1	Nachricht	→		OK
		←	1	OK

Fehler

Kontrollbit: 0	Nachricht	→	✘	Fehler beim Empfänger ⇒ Unerwartetes Kontrollbit zurück senden
		←	1
Kontrollbit: 0	Nachricht	→		Fehler beim Sender
✘		←	0	Fehler beim Sender
Kontrollbit: 0	Nachricht	→		OK
		←	0	OK
Kontrollbit: 1	Nachricht	→	✘	Fehler beim Empfänger ⇒ Unerwartetes Kontrollbit zurück senden
		←	0
Kontrollbit: 1	Nachricht	→		Fehler beim Sender
✘		←	1	Fehler beim Sender
Kontrollbit: 1	Nachricht	→		OK
		←	1	OK

−Table of Contents