Umfang

Dieses Thema kann als Masterarbeit oder Projektarbeit bearbeitet werden.

Empfohlene Vorkenntnisse

  • gute Java Kenntnisse
  • Grundlagen des Compilerbaus
  • Kenntnisse der B Sprache sind erwünscht (zB. durch Besuch der Veranstaltung “Sicherheitskritische Systeme”)

Problem

ProB ist ein Werkzeug zur Validierung formaler Spezifikationen. Diese Software hat viele Parameter und viele Validierungstechniken. In einer vorherigen Arbeit wurde ein Übersetzer von TLA+ nach B entwickelt um TLA+ Spezifikationen mit ProB prüfen zu können. ZB hat TLA+ zwar den TLC Modelchecker von Leslie Lamport aber keinen Animator.

  • Dominik Hansen, Michael Leuschel: Translating TLA + to B for Validation with ProB. IFM 2012: 24-38

Die aktuelle Übersetzung hat einige Einschränkungen, und kann nicht alle TLA+ Typen übersetzen. Auch ist die Anzeige der TLA+ Typen im ProB Animator für TLA+ Benutzer nicht optimal.

Minimalanforderungen

  • Erweiterung von TLA2B um weitere Datentypen

Erweiterungen

  • Verbesserung der grafischen Benutzeroberfläche in ProB
  • Empirische Auswertungen

Kontakt

Professor Michael Leuschel
Raum 25.12.02.60 · michael.leuschel@hhu.de