Formale Verifikation

Startseite
Darstellung von Zustandsmengen   ● Ausgangspunkt: Zustandsdiagramm einer sequentiellen Schaltung 00 01 10 11 0/1 1/0 1/0 1/0 0/0 0/0 1/0 ● Boolesche Ausdrücke (charakteristische Funktionen) charakterisieren Mengen von Zuständen z1z2 ● Beispiel: zwei Zustandsvariablen z1, z2 ● z1 + z2 charakterisiert die Menge {01, 10, 11}   z2 ● z2 charakterisiert die Menge {00, 10}