|
|
Seminar: Advanced Model Checking - Wintersemester 05/06
Übersicht
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.
|
In diesem Seminar wollen wir einige neue Entwicklungen im Bereich Model Checking behandeln.
Als Themenbereiche sind vorgesehen:
1. Real-Time Model Checking
2. Stochastisches Model Checking
3. Model Checking für Prädikatenlogik erster Ordnung
|
|
