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.
AG und EG
00
01
10
11
0/1
0/1
1/0
1/0
1/0
0/0
0/0
1/0
z
1
z
2
M
●
AG(M)
: Alle aktuellen und alle Nachfolgezustände sind
durch
M
charakterisiert.
AG(M)
AG(M)
charakterisiert alle Zustände,
von denen aus
M
nie eintreten kann
(Sicherheitseigenschaft) z.B. es tritt
nie ein, dass alle Ampeln grün sind.
AG(M)
●
EG(M)
: Es gibt mindestens einen Pfad,
auf dem der aktuelle und alle Nachfolgezustände
durch
M
charakterisiert sind.
M
EG(M)
Beispiel: A
G(z+
1
z
2
) =
?
z
1
+z
2
= 0 (leere Menge)