Formale Verifikation
Formale Verifikation
Simulation und formale Verifikation
Werkzeuge der formalen Verifikation
Equivalence-Checking: Problemstellung
Erfüllbarkeitsproblem(Satisfiability,SAT)
SAT1-Problem
SAT-Equivalence-Checker
Graphenisomorphie
Binary Decision Diagrams (BDDs)
Binärer Entscheidungsbaum: Beispiel
Zusammenfassen identischer Teilbäume
Entfernen überflüssiger Knoten
Abhängigkeit der Knotenanzahl von der Entwicklungsreihenfolge
Vorteile der BDDs
Beispiel:ALU(SN74181)
Model-Checking
Symbolic Model Checking
Zustandsmengen
Temporale Logik
Elemente von CTL
CTL-Syntax
AX und EX
AF and EF
AG und EG
Beispiel: Modulo-3-Zähler
Startseite
Hinweis
: Da Javascript ausgeschaltet ist, sind die Grafiken nicht animiert.
AX und EX
M
AX(M)
charakterisiert alle Zustände, die nur
Nachfolgezustände haben, die durch
M
charakterisiert sind.
Ausschnitt aus dem Computation Tree
AX(M)
EX(M)
charakterisiert alle Zustände, von denen aus wenigstens
ein Nachfolgezustand durch
M
charakterisiert ist.
EX(M)
00
01
10
11
0/1
0/1
1/0
1/0
1/0
0/0
0/0
1/0
z
1
z
2
Beispiel:
AX(z
2
)
= ?
z
2
AX(z
2
) = z
1