Verifikation eingebetteter Systeme - Wintersemester 08/09

Übersicht

Beschreibung

Lernziele:

Studierende kennen die Grundfragen der formalen Verifikation im Unterschied zur reinen Simulation von Schaltungen und Systemen und können davon ausgehend wichtige algorithmische Techniken anwenden und gegebenenfalls an neue Bedürfnisse anpassen.

Sie lernen mögliche Gefahren im Falle des fehlerhaften Entwurfs eingebetteter Systeme zu erkennen und das Instrumentarium zum Nachweis und zur Vermeidung solcher Fehler (insbesondere durch formale Methoden) zu beherrschen.

Lehrinhalt:

Viele moderne Produkte basieren auf mikroelektronischen Komponenten. Oftmals ist das korrekte Funktionieren dieser Produkte lebenswichtig, etwa in Medizintechnik oder Autoelektronik. Daher werden hohe Anforderungen an die Qualität der darin eingesetzten mikroelektronischen Systeme gestellt. Die Anforderungen lassen sich in drei Gruppen unterteilen: (1) Das System muss korrekt entsprechend der Spezifikation entworfen sein. (2) Das gemäß Entwurf physikalisch gefertigte System soll zum Zeitpunkt seiner Herstellung fehlerfrei funktionieren. (3) Darüber hinaus soll das System für einen gegebenen Zeitraum zuverlässig (d.h. ohne Ausfall) eingesetzt werden können.

Während Anforderung (2) durch Testmethoden und Anforderung (3) durch Methoden zur Erhöhung der Ausfallsicherheit behandelt werden, spielen für die Einhaltung von Anforderung (1) Verifikations- und Validierungsmethoden eine Rolle. Der Schwerpunkt der Vorlesung liegt auf Verifikations- und Validierungsmethoden für digitale Komponenten und auch für hybride Systeme (d.h. Systeme, die auf einem Zusammenspiel von digitalen Komponenten mit einer kontinuierlichen Umgebung beruhen). Dabei interessiert sowohl der formale Nachweis von Systemeigenschaften als auch die Übereinstimmung des Entwurfs im Vergleich zu einer gegebenen Spezifikation. Es werden zunächst verschiedene existierende Basistechniken zur formalen Verifikation vorgestellt, wie z.B. Decision Diagrams und SAT-Solver. Darauf aufsetzend werden Ansätze zum Äquivalenzvergleich sowie zur Eigenschaftsprüfung beschrieben. Schließlich werden erweiterte Techniken betrachtet, die auch die Verifikation Hybrider Systeme ermöglichen.

Kommentar

Spezialvorlesung