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.

Die Vorlesung finde in Präsenz statt. Es werden Videos der Folien und des Tons mitgeschnitten. Übungen sind zur Zeit online.

Die Vorlesungsunterlagen findet man hier, wenn man sich über "intern" eingeloggt hat und diese Seite wieder angesteuert.

Sonstiges
Zuordnung im Masterstudiengang Informatik: M-HSE-SV

aber auch wählbar in den Modulen: M-Theo-IDS-A/B , M-WR-IDSA/B