Kombination formaler und semiformaler Techniken zur Verifikation von C-basierten Systembeschreibungen

点击翻译按钮获取中文摘要

Ziel dieses Projektes ist, die Vorteile der klassischen Simulation wie Skalierbarkeit mit den Vorteilen formaler Methoden, z.B. vollständige Funktionsüberprüfung und bewährte, auf formalen Sprachen basierte Spezifikationstechniken, zu kombinieren. So können beispielsweise kritische Systemeigenschaften formal spezifiziert werden und in einem ersten Schritt "on-the-fly", d.h. parallel zum Ablauf einer klassischen Simulation überprüft werden. Damit lassen sich mit wenig Rechenaufwand bereits einfache Fehler finden. In einem späteren Schritt sollen dann Partitionierungstechniken entwickelt werden, mit denen die zu testenden Stimuli und das zu verifizierende System so aufgeteilt werden können, daß sich Teile davon mit Simulation validieren lassen und andere Teile mit formalen Methoden verifiziert werden können. Außerdem sollen auch Methoden der symbolischen Simulation Verwendung finden, um die bereits angesprochenen Kombinationstechniken weiter auszubauen. Diese kombinierten Validationstechniken sollen in einem Werkzeug prototypisch implementiert werden. Diese kombinierte Verifikation soll möglichst früh auf hohen Abstraktionsebenen stattfinden, um den nachfolgenden Entwurf in die richtigen Bahnen zu leiten. Zu diesem Zweck werden Systembeschreibungen als Validationsgrundlage herangezogen. In diesem Projekt soll aufgrund der zunehmenden Verbreitung eine C-basierte Systembeschreibungssprache verwendet werden. Zum Einen erhält man damit eine große Zahl von Systemen, die zu Testzwecken herangezogen werden können. Zum Anderen ergibt sich die Möglichkeit, die im Projekt erarbeiteten Methoden direkt im industriellen Kontext zu testen.