Processing math: 100%

Wiki

A universe of ideas

User Tools

Site Tools


uni:6:fsv:start

This is an old revision of the document!


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

  • Rekursive Funktion KNF
    • Rein
      • (Nicht-Normalisierte) Formel
    • Raus
      • Neuster (frischer) Variablenname
      • KNF
  • C ist frische Variable
  • Regel: Cϕ als KNF
    1. Tabelle Erstellen
    2. Bei 0: Veroderung (Disjunktion) erstellen (A=0A / A=1¬A)
    3. Verodrungen verunden (Konjunktion)
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

  • “ist ϕ erfüllbar?”
  • Entscheidungsproblem (NP-Hart)
  • Nur für KNF
  • Erweiterung auf nicht KNF: Tseitin Übersetzung
  • Erweiterung auf Äquivalenz von ϕ und ψ: ¬(ϕψ) 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 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

  • 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=(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

  • 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(EFpqp,sleep)
  • Fairness: “Gute Eigenschaft” gilt für alle fairen Abläufe

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

  • Zustandsmenge: {(False,True),(True,False),(True,True)}
  • Transitionsrealtion: {((Fals,True),(True,False)),}

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

  • (AE)(GF) vertauschen und 2xnegieren
    • AG(ϕ)¬EF(¬ϕ)
    • AF(ϕ)¬EG(¬ϕ)
    • EF(ϕ)¬AG(¬ϕ)
    • EG(ϕ)¬AF(¬ϕ)
  • AG(ϕψ)AG(ϕ)AG(ψ)
  • AF(ϕ)A[Uϕ]
  • EF(ϕ)E[Uϕ]
  • A\[ϕUψ\]¬(E[¬ϕU(¬ϕ¬ψ)]EG(¬ϕ))

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

  • AF(ϕ), wo ..
    • ϕ
    • Alle Nachfolger sind AF(ϕ)
  • E[ϕUψ], wo ..
    • ψ
    • ϕ und Folgezustand mit E[ϕUψ]

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

SMV

Teile

  1. MODULE
  2. VAR
  3. ASSIGN
  4. INIT
  5. TRANS
  6. SPEC
  • 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;
  • :=;
uni/6/fsv/start.1405261668.txt.gz · Last modified: 2020-11-18 18:10 (external edit)