KIT | KIT-Bibliothek | Impressum | Datenschutz

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

Giese, Martin; Kempe, David; Schoenegge, Arno

Abstract:

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


Volltext §
DOI: 10.5445/IR/28697
Cover der Publikation
Zugehörige Institution(en) am KIT Fakultät für Informatik – Institut für Logik, Komplexität und Deduktionssysteme (ILKD)
Publikationstyp Buch
Publikationsjahr 1997
Sprache Deutsch
Identifikator urn:nbn:de:swb:90-AAA286972
KITopen-ID: 28697
Erscheinungsvermerk Karlsruhe 1997. (Interner Bericht. Fakultät für Informatik, Universität Karlsruhe. 1997,16.)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page