Forschungsthemen
[GB] Evaluierung verschiedener Model Checker für die Modellprüfung von Qualitätseigenschaften
Bei der Erstellung moderner Informationssysteme nimmt die Zusicherung von Qualitätseigenschaften wie z.B. Sicherheit und Verlässlichkeit mittlerweile eine zentrale Rolle ein. Ein formaler Nachweis dieser Eigenschaften ist oft erwünscht und meist sogar unumgänglich. Zu diesem Zweck werden im Zusammenhang mit modellbasierten Entwicklungsmethoden so genannte Model Checker (z.B. SPIN oder UPPAAL) eingesetzt, um den formalen Nachweis dieser Eigenschaften zu erbringen.
Ziel der Arbeit ist es, eine möglichst große Auswahl verschiedener Model Checker anhand eines Fallbeispiels hinsichtlich ihrer Funktionalität zu vergleichen. Dabei sollen insbesondere folgende Eigenschaften betrachtet werden:
- Art der Spezifikation der Systembeschreibung
- Art der Formalisierung der Systemeigenschaften
- Mächtigkeit der Modellprüfung
Betreuer: Mirko Seifert