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).