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.
AF und EF
M
AF(M)
●
AF(M)
: Zustände, von denen aus
M
unvermeidbar ist
AF(M) charakterisiert alle Zustände,
von denen aus M irgendwann sicher
eintritt (Lebendigkeitseigenschaft),
z.B. irgendwann zeigt die Ampel grün.
M
●
EF(M)
:
M
ist erreichbar
(jetzt oder später)
EF(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:
EF(z
1
z
2
) =
?
"Von welchen Zuständen aus ist es möglich,
wieder in den Anfangszustand zu kommen?"
z
1
z
2
EF(z
1
z
2
)=z
1
+z
2
siehe AG und EG