Umfang

Der Umfang der Arbeit lässt sich so anpassen, dass das Thema als Bachelorarbeit, Projektarbeit oder Masterarbeit bearbeitet werden kann.

Empfohlene Vorkenntnisse

  • gute Kenntnisse in Prolog (z.B. durch Besuch der Veranstaltung “Einführung in die logische Programmierung”)
  • gute Kenntnisse in Compilerbau (z.B. durch Besuch der Veranstaltung “Compilerbau”)
  • Kenntnisse der B Sprache (z.B. durch Besuch der Veranstaltung “Sicherheitskritische Systeme”)

Problem

B ist eine Spezifikationssprache, die vorallem für sicherheitskritische Systeme verwendet wird. ProB ist ein Validierungstool für Softwarespezifikationen insbesondere für die B Methode. Das Tool selbst ist in der Programmiersprache Prolog implementiert und unterstützt Validierungstechniken wie etwa Animation und Model Checking. Im gewöhnlichen Workflow werden B Maschinen schrittweise modelliert, verfeinert und verifiziert. Sobald die letzte Verfeinerungsstufe (eine low-level Teilmenge von B, auch B0 genannt) erreicht wird und alle Verfeinerungen verifiziert sind, wird anschließend Code für die Ausführung generiert. B2Program ist ein Codegenerator von B nach höheren Programmiersprachen. Aktuell werden die imperativen Programmiersprachen Java, C++ und Python unterstützt. Verglichen mit den meisten anderen Codegeneratoren werden auch B Maschinen auf abstrakteren Ebenen unterstützt. Somit erfordert die Codegenerierung keine Verfeinerung bis auf die B0 Ebene (eine low-level Teilmenge von B).

Die Aufgabe dieser Arbeit besteht darin B2Program um die logische Programmiersprache Prolog zu erweitern, sodass B Modelle nach Prolog für die Verwendung in ProB übersetzt werden können. Ein interessanter Aspekt besteht darin, die Performance der B Modelle mit der Übersetzung nach Prolog zu vergleichen.

Minimalanforderungen

  • funktionsfähige Erweiterung von B2Program um Prolog
  • Prolog Dateien müssen in ProB verwendbar sein

Erweiterungen

  • empirische Auswertung der Performance mit Vergleich zu ProB
  • Evaluation möglicher Darstellungen für Mengen und Relationen

Bemerkungen

Dieses Thema ist vergeben.

Kontakt


Fabian Vu
Raum 25.12.02.50
Fabian.Vu@hhu.de