Am

• 29.10. finden 2 Stunden Vorlesung statt.
• 30.10. finden 2 Stunden Vorlesung statt.
• 5.11. finden 2 Stunden Übung statt.
• 6.11. fällt die Veranstaltung aus.

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.

Vorlesung

Di. 12:15 - 13:45 Uhr, Seminarraum SR 307, Robert-Mayer-Str. 11-15

Mi. 13:00 - 13:45 Uhr, Seminarraum SR 307, Robert-Mayer-Str. 11-15

Übung

Mi. 12:15 - 13:00 Uhr, Seminarraum SR 307, Robert-Mayer-Str. 11-15

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

Sonstiges

Zuordnung im Masterstudiengang Informatik 2019 zum Modul M-SV. Das Modul ist  den Spezialisierungen: Algorithmen und Komplexität, Green IT / Hochleistungsrechnen zugeordnet.

In der PO 2011in den Modulen: M-HSE-SV M-Theo-IDS-A/B , M-WR-IDSA/B