Lecture: Verifikation eingebetteter Systeme

Department Computer Engineering
Professoren Prof. Dr. habil. Kropf
Dr. Ruf
Tutor Dr. LĂ€mmermann
Heckeler
Lecture Donnerstag / 17:00
Room A301 Sand 13
Preliminary Discussion         13.10.2011, 17:00, A301
Beginning 13.10.2011, 17:00, A301
Amount 2 SWS / 3 LP
Amount of Exercices 1 LP
Amount of Lab 4 LP
Exam Combination         V+Ü, V+Ü+P
Examination Subject      Technische Informatik
Homepage https://cis.informatik.uni-tuebingen.de/ves-ws-1112/
LSF Entry Verifikation eingebetteter Systeme

Description

 

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 

 

Comment

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