Vorlesung: Systemverifikation

Inhalt

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.

Lernziele: Es soll ein Verständnis zur effektiven automatischen Verifikation von Systemen entwickelt werden. Durch Rechnerübungen wird der praktische Umgang und die dabei auftretenden Herausforderungen von automatischer Verifikation erlernt. Schließlich sollen die Studierenden in der Lage sein, Verifikationsmethoden zu beurteilen und für den richtigen Einsatz auswählen zu können.

Voraussetzungen: Die Veranstaltung SV ist Pflichveranstaltung des Moduls M-SV (6 CP) im Gebiet IDS, Spezialisierung SyEn

Teilnahmebedingungen / erforderliche Kenntnisse: Keine

Nützliche Vorkenntnisse: Kenntnisse aus dem Bereich des rechnergestützten Entwurfs mikroelektronischer Schaltungen.

Termine

Vorlesung:
Di. 12:00-14:00 Uhr, Raum 307
Mi. 12:00-13:00 Uhr, Raum 307

Übung:
Mi. 13:00-14:00 Uhr, Raum 307

Sonstiges

Zuordnung im Masterstudiengang Informatik:
M-SV

Zuordnung im Diplomstudiengang Informatik:
PT3 (alt P5, P6), Voraussetzungen: Vordiplom