Processing math: 100%

Table of Contents

Formale Spezifikation und Verifikation

Formal = Mittels Logik

Propositionallogik

Syntax

Propositionale Variablen A,B,C,
Junktoren ¬,,,,
Formel ϕ,ψ,
Konstanten ,

Semantik

Belegung η
Foo ϕη
Bar &,
Tautologie η:ϕη
Erfüllbar η:ϕη
Unerfüllbar η:¬ϕη
Äquivalent η:ϕη=ψη
Erfüllbarkeitsäuivalenz (ϕ und ψ sind erfüllbar)(ϕ und ψ sind unerfüllbar)

Normierung

Literal A und ¬A
Minterm Konjunktion: (Die wenigsten Belegungen sind )
Maxterm / Klausel Disjunktion: (Die meisten Belegungen sind )
KNF ()()
DNF ()()
ϕ … KNF Größe Zeit
Äquivalent exponentiell ?
Erfüllungsäuivalent linear polynomiell

Tseitin Übersetzung

Nur erfüllungsäquivalent

KNF(A)=(A,)
KNF(¬ϕ)=let (B,Γ)=KNF(ϕ) in(C,Γ(CB)(¬C¬B))
KNF(ϕ1ϕ2)=let (B1,Γ1)=KNF(ϕ1) inlet (B2,Γ2)=KNF(ϕ2) in(C,Γ1Γ2(¬CB1B2)(C¬B1)(C¬B2))

SAT-Solver

SAT

DPLL-Algorithmus

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 das selbe liefern, dann darf ¬((f1(x)f1(x))(f2(x)f2(x))) keine Lösung liefern.

Nebenläufige Systeme

Zeit
0 1 n-1
Zustand z1 xzt
z2
tzZzz¬(xztxzt) Zu jeder Zeit ist nur ein zustand gesetzt
zIxz0 Einer der Startzustände
n2t=0zzxztxz(t+1) Zu jeder Zeit führt ein Zustand in einen Folgezustand
n1t=0zVxzt Zu einer Zeit ist ein verbotener Zustand erreicht

Dieses System darf keine Lösung haben.

BDD

nichtreduzierter BDDs

reduzierte BDDs (zusätzlich)

nichtreduziert → reduziert

BDDs sind eindeutig: Gleiche Funktion ⇒ isomorphe BDDs

Shannon-Zerlegung: f=(xf[x:=])(¬xf[x:=⊥])

Negation: True und False vertauschen

Variable setzen:

  1. ersetzen/umlenken
  2. reduzieren

Zweistellige Operationen: Rekursiv (x(f[x:=]g[x:=]))(¬x(f[X:=⊥]g[x:=⊥])) (Gehe die Variablen der reihe nach durch. Ersetze die Nachfolger durch aus den True-Zweigen und durch aus den False-Zweigen.)

Alle möglichkeiten einer Variablen probieren: x:f:=f[x:=]f[x:=⊥]

Optiomierungen

Es fehlen nebenläufige Systeme!!!

Model checking

Arten

Dinge die Interessieren

CTL

Propositionale Variablen p,q, Jedes Aussgenlogische Formel ist CTL!
Junktoren ¬,,,,
Formel ϕ,ψ,
Konstanten ,
Foo AX,EX,A[ϕUψ],E[ϕUψ],AGϕ,AFϕ,EGϕ,EFϕ

AG¬EF(¬ϕ)

AAuf allen Pfaden gilt …
EAuf (mindestens) einem Pfad gilt …

…in…

XNext… (mindestens) einem unmittelbar folgenden Zustand
FFinal… (mindestens) einem folgenden/selben Zustand
GGlobaly… allen folgenden/selben Zuständen
UUntil… allen folgenden/selben Zuständen ϕ, bis ψ gilt.
ψ kann bereits im selben gelten

Transitinssystem

(S,)

Interpretationen

Tr(I) (S,) Transitionsystem Durch I festgelegt
I(p) S Zustände in denen p gilt
sIp {True,False} Aussage: p ist in Zustand s gesetzt
I(ϕ) S Zustände in denen ϕ gilt Ableitbar
sIϕ {True,False} Aussage: ϕ ist in Zustand s gesetzt

Interpretation enthält keine Formel.

Äquivalenz

Labeling Algorithmus

  1. Formel umformen (nur noch ¬,,,AF,E[U])
  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 ..

Effizienter: EG(ϕ) anstatt AF(ϕ)

  1. ¬ϕ 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)

Fairnes

Alle interessierenden Zustände können immer unendlich offt erreicht werden.

Abwandlung des Labeling Algorithmuses:

Encoding of CTL in BDD

BDD ist ein Bitvektor und daher kann ich ein Transitionsystem eincodieren, sowie ein ϕ.

http://nicta.com.au/__data/assets/pdf_file/0018/14814/lecture4-mc2.pdf

ToDo

LTL

Propositionale Variablen p,q, eingeschränktes CTL!
Junktoren ¬,
Formel ϕ,ψ,
Konstanten
Foo Xϕ,Fϕ,Gϕ,ϕUψ

Büchi Automat

(Σ,T,I,E,δ)

Σ Menge Alphabet
Z Menge Zustände
I Menge Anfangszustände
E Menge Endzustände
δ Relation Zustandsübergänge

L=(ba)ω (wenn a immer wieder vorkommen muss)

ω FG Unendlich offt vorkommen
GF Endlich offt vorkommen

Typanalyse

While Programm

Datenflussgleichung

“Erreichbare Definitionen” (Reachable Definitions)

“Verfügbare Ausdrücke” (Available Expressions)

“Lebendige Variablen” (Live Variables)

RDentry() RDexit()
1 (x, ?), (y, ?)
2
3

So lange ausfüllen, bis nichts mehr geht.

Das geht, weil Fixpunkte und Knaster-Tarski-Theorem

SMV

Teile

  1. MODULE
  2. VAR
  3. ASSIGN
  4. INIT
  5. TRANS
  6. SPEC
  7. JUSTICE/FAIRNESS

MODULE

MODULE main

– oder –

MODULE p(x, y, z)

VAR

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

ASSIGN

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

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

INVAR

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

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

Supremum

s=U

Monotonie

Fixpunkt

Dazu muss F(x) monoton sein.

Probleme

Semaphor

Alternating Bit Protocol

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