Automatisierte Dokumentation von formalen Modellen und ihrer Verifikation/Validierung
Der Umfang der Arbeit lässt sich so anpassen, dass das Thema als Bachelorarbeit oder Projektarbeit bearbeitet werden kann.
Empfohlene Vorkenntnisse
- gute Kenntnisse in Java
- Kenntnisse in Compilerbau könnten hilfreich sein (z.B. durch Besuch der Veranstaltung “Compilerbau”)
Problem
ProB2-UI ist eine graphische Nutzeroberfläche für den Animator, Model Checker und Constraint Solver ProB. Mithilfe von ProB2-UI ist es möglich ein Projekt bestehend aus mehreren formalen Modellen anzulegen. Für jedes der Modelle können Verifikation - und Validierungstasks im Projekt persistiert werden. Ebenfalls im Projekt werden neuerdings auch Anforderungen persistiert. Die Aufgabe dieser Arbeit besteht darin, formale Modelle und ihre Verifikation/Validierung automatisiert zu dokumentieren. Dies soll dadurch erreicht werden, dass ein LaTex Dokument für das Projekt, für die formalen Modelle, sowie für ihre Verifikations - und Validierungstasks generiert wird.
Minimalanforderung
- Generierung eines LaTex Dokuments aus einem Projekt/Modell
- Anbindung in ProB2-UI
Erweiterungen:
- Generierung der Dokumentationen für Verifikationen/Validierungen des Modells (Validierungstasks, Validierungsobligationen, Anforderungen, …)
- Demonstration anhand von Beispielen
Bemerkungen:
Dieses Thema ist vergeben.
Kontakt
Fabian Vu
Raum 25.12.02.50
Fabian.Vu@hhu.de