A Coverification Framework

AUTOR(ES)
DATA DE PUBLICAÇÃO

1999

RESUMO

In dieser Dissertation wird eine Koverifikations-Umgebung (coverification fra-mework CVF) präsentiert. CVF ist geeignet für die Validierung von Systemen die aus Hardware und Software bestehen. Das Werkzeug profitiert von der partitionierten Natur der HW/SW-Systeme, da die Eigenschaften der Systeme modular verifiziert werden. Die Modellprüfung (model checking) ist die formale Verifikations-Methode, die in CVF angewendet wird. Die Methode wurde angepaßt, so daß HW/SW-Systeme verifiziert werden können. Um dem Benutzer Arbeit zu ersparen, werden einige Eigenschaften abgeleitet, die verifiziert werden müssen. Zusätzlich bietet CVF eine benutzerfreundliche Umgebung (framework) für die Spezifikation von eingebetteten Systemen (embedded Systems) an. Außerdem können temporale logische Formeln geprüft werden. Da eingebettete Systeme komplex und normalerweise steuerungsorientiert (control-dominated) sind, ist die Anwendung von endlichen Zustandsautomaten (FSM: finite state machines) nicht geeignet wegen des bekannten Problems der Zustandsexplosion (state explosion problem). Aus diesem Grund sind in CVF einige Methoden zur Umgehung dieses Problems eingesetzt worden. Die Methoden sind Reduzierung des Zustandsraums durch Halbordnung (partial-order reduction), modulare Verifikation, symbolische Techniken und Abstraktion. Eine partitionierte HW/SW-Spezifikation is die Eingabe in das Koverifikations-Werkzeug CVF ist eine Werkzeug, das nach der Partitionierung angewendet wird. Die partitionierte Spezifikation wird in PROL geschrieben. PROL ist die Eingangssprache für CVF und ist mit einigen besonderen Kon-strukten für HW/SW-Systeme und die Spezifizierung von Eigenschaften ausgerüstet. Durch eine Art symbolischer Ausführung werden die Ereignisse und Systemverhältnisse identifiziert. Das Verhalten wird als eine Menge von Relationen modelliert, die basierend auf einer Semantik der Halbordnung in logische Formeln (durch BDDs implementiert) übersetzt werden. In CVF werden die Eigenschaften partitioniert, auf Eigenschaften, die sich auf Ereignisse (events) beziehen, übersetzt und modular geprüft. Zusätzliche Eigenschaften, die das Zeitverhalten (timing) und die Ressourcen (resources) betreffen, werden verifiziert, um die Korrektheit des Systems zu garantieren. Diese Eigenschaften werden automatisch aus dem Einschränkungen (con-straints) abgeleitet, die als Eingabe für die Kosynthese benutzt wurden. Die Eigenschaften werden durch den Benutzer spezifiziert, der entweder einige Eigenschaftsmuster (property pattern,s), die das Werkzeug anbietet oder POMTL, eine temporale Logik für POMs, einsetzen kann. Die Verifikation dieser Eigenschaften wird durch einen POM-Prüfer durchgeführt, der aus einem Modell-Prüfer besteht, der POMs verifizieren kann. Dieser Prüfer berichtet dem Benutzer, ob sein HW/SW-System korrekt ist. Die Korrektheit ist bezogen auf die Eigenschaften, die durch den Benutzer spezifiziert wurden und die Eigenschaften, die automatisch auf Grund der Zeit- (timing-) und Ressourcen-Einschränkungen generiert wurden. Da CVF alle mögliche Systemvariablen in Betracht zieht, können Fehler wie Bereichsfehler (boundness errors) von Variablen zur Kompilierungszeit entdeckt werden. Darüberhinaus kann CVF erkennen, ob das System Verklemmungen (deadlocks) oder unendliche Schleifen hat, ohne daß der Benutzer explizit diese Eigenschaften spezifiziert.

ASSUNTO(S)

model checking sistemas de computacao hw/sw codesign informática concurrency models formal verification

ACESSO AO ARTIGO

Documentos Relacionados