Struktur von Verifikations-Werkzeugen

Zusammenfassung

Im letzten Kapitel soll kurz auf die prinzipielle Struktur von Verifikations-Werkzeugen eingegangen werden. Das bei der Entwicklung eines derartigen Werkzeuges zu berücksichtigende Wissen kann nach Abb. 22.1 drei verschiedenen Kategorien zugeordnet werden:

• auf der Daten-Ebene werden die wesentlichen Eigenschaften der zu verifizerenden Hardware repräsentiert;

• die Wissensbasis-Ebene enthalt das grundsätzliche Wissen über die Eigenschaften der Modellvorstellungen, z.B. die Axiome der booleschen Algebra, sowie zusätzliche “nützliche” Hilfssätze, z.B. die Äquivalenzen der Abb. 11.6;

• schließlich die Kontroll-Ebene, die ein Wissen darüber enthält, wann welche Axiome und Hilfssätze anzuwenden sind.