KIV zur Verifikation von ASM-Spezifikationen am Beispiel der DLX-Pipelining Architektur

In der hier beschriebenen Fallstudie wurde das KIV-System (Karlsruhe
Interactive Verifier) zur Verifikation von ASM-Spezifikationen
(Abstract State Machines) eingesetzt. Diese Fallstudie behandelt die
von Boerger & Mazzanti aufbereitete Verifikation der
DLX-Pipelining-Architektur. Wir geben Details der formalen
Spezifikation und Verifikation mit KIV, schaetzen den damit
verbundenen Arbeitsaufwand ab und skizzieren kleinere
Unzulaenglichkeiten der informellen Verifikation, welche durch die
Formalisierung aufgedeckt werden konnten.

Zudem wird von einer Erweiterung des KIV-Systems um zwei neue
Beweistaktiken berichtet, welche speziell auf die effiziente
Verifikation von ASM-Spezifikationen zugeschnitten sind. Diese wurden
im Rahmen der hier behandelten Fallstudie erarbeitet, implementiert
und eingesetzt