Vorlesung: Verifikation eingebetteter Systeme

Lehrstuhl Technische Informatik
Dozenten Prof. Dr. habil. Kropf
Dr. Ruf
Vorlesung Donnerstags, 17:15 - 19:00 Uhr
Raum A302 Sand 13
Vorbesprechung         23.10.2008 A302 Sand 13
Umfang 2 SWS / 3 LP
Voraussetzungen         5 ff.
Pr├╝fungsfach      Technische Informatik
Homepage https://cis.informatik.uni-tuebingen.de/ves-ws-0809/
Eintrag im LSF 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).