Umfang

Dieses Thema kann als Projektarbeit oder Masterarbeit bearbeitet werden.

Empfohlene Vorkenntnisse

  • sicherheitskritische Systeme
  • B / Event-B
  • Prolog, Java

Problemstellung

B und Alloy sind formale Spezifikationssprachen welche z.B. für die Modellierung sicherheitskritischer Systeme verwendet werden. Beide Sprachen haben einige Unterschiede. Alloy z.B. übersetzt Constraints nach SAT und verwendet SAT Solver für die Lösungsfindung. Dies kann Vor- und Nachteile haben: es werden nur endliche Mengen unterstützt und es können Integer Overflows auftreten; dafür können relationale Constraints oftmal sehr schnell gelöst werden. Wir haben eine Übersetzung von Alloy Version 5 nach B formalisiert und in Prolog für das ProB Werkzeug implementiert. Somit können Alloy Modelle mit ProB’s Constraint Solver gelöst werden. Diese Übersetzung hat einige Vorteile im Vergleich zu dem Alloy Analyzer gezeigt, z.B. für das Lösen von Integer Constraints. Im Rahmen dieser Arbeit soll die Übersetzung und Implementierung für die neue Version 6 von Alloy erweitert werden. Dabei soll auf der bestehenden Implementierung aufgebaut werden. In Alloy’s Version 6 sind einige neue Konstrukte hinzugekommen welche ebenso nach B übersetzt und mit ProB’s Constraint Solver gelöst werden können. Es ist Teil der Arbeit sich in die Alloy Sprache einzuarbeiten.

Minimalanforderungen

  • Erweiterung der bestehenden Implementierung um eine Übersetzung von Alloy 6 nach B
  • Integration in ProB
  • Performanceauswertung

Erweiterungen

  • Performanceoptimierung
  • Übersetzung von Traces bzw. Orderings als B Maschinenoperationen

Kontakt

Joshua Schmidt
Raum 25.12.02.52 · joshua.schmidt@hhu.de