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:
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 Softwareprotokolle und 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. Eigenschaftsprüfung wird zur Verifikation sowohl von digitalen Komponenten als auch von Softwareprotokollen und Hybriden Systemen verwendet.

Prof. Dr. Bernd Becker
Institut für Informatik
E-Mail: becker(at)informatik.uni-freiburg.de
Telefon: +49 (0) 761 203-8141

Prof. Dr. Christoph Scholl
Institut für Informatik
E-Mail: scholl(at)informatik.uni-freiburg.de
Telefon: +49 (0) 761 203-8152

Haben Sie Interesse an diesem Kurs?
Hier gehts zur Anmeldung.
Oder kontaktieren Sie uns einfach bei weiteren Fragen.

