Materialien
Vorlesungsmaterial
Leistungsnachweis
Prüfungskriterien Seminar: Theoretical Foundations of Model Checking - Wintersemester 06/07
Übersicht
| Beschreibung |
Aufgrund der immer größer werdenden Komplexität von eingebetteten Systemen - beispielsweise sind heutzutage in einem einzigen Auto mehrere Dutzend Prozessoren miteinander verschaltet - wird der Bedarf für formale Korrektheitsbeweise immer größer. Dieser wird noch verstärkt durch die Tatsache, dass viele der Systeme in sicherheitskritischen Bereichen eingesetzt werden und bei fehlerhafter Funktionsweise oft Menschenleben in Gefahr sind. Model Checking ist eine Methode, mit der Eigenschaften eines Systems, die in einer formalen Logik spezifiziert sind, nachgewiesen werden können. Seit den ersten Arbeiten Mitte der 80er Jahre ist ein enormer Fortschritt zu verzeichnen, insbesondere im Hardware-Bereich. Heutzutage haben alle wichtigen Hardwarehersteller Model-Checking Gruppen, die Model-Checkers für die Verifikation von Schaltkreisen entwickeln und anwenden. |
| Kommentar |
In diesem Seminar wollen wir uns auf die theoretischen Grundlagen von Model Checking konzentrieren. Ein Themenbereich beschäftigt sich mit der Bisimulationen, ein anderer mit hybriden Automaten. Teilnehmer sollten Kenntnisse in Logik und theoretischer Informatik mitbringen. |