Vorlesung: Verifikation eingebetteter Systeme

Beschreibung

Der Entwurf moderner datenverarbeitender HW/SW-Systeme stellt eine immer größer werdende Herausforderung für die Systementwickler dar. Wachsender Zeitdruck, höhere Anforderungen an die Korrektheit und steigende Systemkomplexität machen den Systementwurf zu einer sehr komplexen Aufgabe. Erschwerend kommt hinzu, daß diese Systeme oft heterogen arbeiten, das bedeutet, daß sowohl Hardware- als auch Softwarekomponenten gemeinsam eingesetzt werden. Diese Faktoren führen dazu, daß man nach neuen Konzepten und Beschreibungsmitteln sucht, um eingebettete HW/SW-Systeme oder SoC-Designs (system-on-chip) bereits auf hohen Abstraktionsebenen zu beschreiben, zu verifizieren (z.B. durch Simulation) und automatisch zu synthetisieren (d.h. HW- und Codedesign).

In dieser Vorlesung werden die Grundlagen für die Verifikation eingebetteter Systeme beschrieben:

1. Verifikationszyklus
2. Systembeschreibungen und Modelle
3. Datenstrukturen zur Repräsentation
4. Eigenschaftsspezifikationssprachen (LTL, CTL, PSL).
5. Außerdem werden wir die wichtigsten in der Industrie eingesetzten Methoden besprechen:
   • Simulation
   • Äquivalenzprüfung
   • symbolische Modellprüfung/symbolische Simulation
   • zeitbegrenzte Modellprüfung mit SAT-Methoden
   • semiformale Ansätze und kombinierte Techniken

Bemerkung

Die Dozenten haben einschlägige Erfahrungen im Entwurf und der Verifikation von Systemen im industriellen Umfeld (Bosch/IBM).