Codegenerierung von B nach Prolog
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