Vorlesung: Verifikation eingebetteter Systeme

Lehrstuhl Technische Informatik
Dozenten Prof. Dr. habil. Kropf
Dr. Ruf
Betreuer Dr. L├Ąmmermann
Heckeler
Vorlesung Donnerstag / 17:00
Raum A301 Sand 13
Vorbesprechung         13.10.2011, 17:00, A301
Beginn 13.10.2011, 17:00, A301
Umfang 2 SWS / 3 LP
Umfang der ├ťbung 1 LP
Umfang des Praktikums 4 LP
Pr├╝fungskombination         V+├ť, V+├ť+P
Pr├╝fungsfach      Technische Informatik
Homepage https://cis.informatik.uni-tuebingen.de/ves-ws-1112/
Eintrag im LSF Verifikation eingebetteter Systeme

Beschreibung

 

Der Entwurf moderner eingebetteter Systeme (HW/SW-Systeme) stellt durch den wachsenden Zeitdruck, den h├Âhere Anforderungen an die Korrektheit und die steigende Systemkomplexit├Ąt eine immer gr├Â├č er werdende Herausforderung f├╝r die Systementwickler dar. Es handelt sich dabei um Systeme, die in sicherheitskritischen Anwendungen (Flug-/ Raumfahrt, KFZ-Technik, Produktionssteuerung, Haus- und Medizintechnik) eingesetzt werden. Damit vertrauen wir ihnen das an, was uns am wertvollsten ist, unser Leben und unser Geld. Erschwerend kommt hinzu, dass diese Systeme oft heterogen arbeiten, das bedeutet, dass sowohl Hardware- als auch Softwarekomponenten gemeinsam eingesetzt werden. Diese Faktoren f├╝hren dazu, dass eingebettete HW/SW-Systeme oder SoC-Designs (system-on-chip) auf den verschiedenen Abstraktionsebenen effizient verifiziert (Simulation oder formale Verifikation) werden m├╝ssen.

Um diesen Anforderungen gerecht zu werden, mu├č im industriellen Entwurfszyklus der Aufwand zur Verifikation dieser Komponenten st├Ąndig gesteigert werden (bereits heute gehen bis zu 80% des Entwicklungsaufwandes zu Lasten der Verifikation).

 

Da allein simulationsbasierten Techniken bei der Fehlersuche von komplexen eingebetteten Systemen nicht mehr ausreichen, werden immer h├Ąufiger formale Beweismethoden hinzugenommen. Um diese Techniken auch f├╝r einen Entwerfer nutzbar zu machen, werden insbesondere automatische Beweistechniken bevorzugt. In dieser Vorlesung werden die Grundlagen f├╝r die Verifikation eingebetteter Systeme beschrieben:

  • Systembeschreibung und Modelle
  • Eigenschaftsspezifikationssprachen (LTL, CTL, PSL)
  • 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
    • usw. ...
  • Normen und der Verifikationszyklus

Voraussetzungen: Semester 5 ff.

Eintrag im LSF

- Vorlesung: Verifikation eingebetteter Systeme

- Praktikum: Praktikum zu Verifikation eingebetteter Systeme 

 

Bemerkung

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