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