Die Vorlesung behandelt Verfahren zur Verifikation von digitalen und
analogen Systemen. Verifikation ist die systematische Sicherstellung
gewünschter Systemeigenschaften. Formale Verifikation nutzt dabei
spezielle Techniken, um das Einhalten der spezifizierten Eigenschaften
zu beweisen. Es werden Grundlagen, Algorithmen und deren Realisierung
sowohl im Rahmen der Äquivalenzbeweise als auch der Eigenschaftsbeweise
behandelt. Als Spezifikationsbeschreibungen werden ausgehend von
Boolescher Logik, über Linear Temporal Logic (LTL), auch Computation
Tree Logic (CTL) betrachtet. Neben den eigentlichen Verfahren und
Algorithmen werden Modellierungsmöglichkeiten und methodisches Vorgehen
bei der Hardwareverifikation erläutert. Desweiteren wird ein Bezug zur
Verifikation von Softwaresystemen hergestellt. Inhalte der Veranstaltung
sind u.a.: Formale Verifikation; Spezifikationsbeschreibungen;
Systemdarstellungen und Modellierung, Äquivalenzbeweise,
Eigenschaftsbeweise.
- Trainer/in: Lars Hedrich
- Trainer/in: Ulrike Knauf
- Trainer/in: Sascha Schmalhofer