TLC4B Übersetzung von B nach TLA+ erweitern
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. In einer vorherigen Arbeit wurde ein Übersetzer von B nach TLA+ entwickelt um B Spezifikationen mit dem TLC Modelchecker von Leslie Lamport zu prüfen.
-
Dominik Hansen, Michael Leuschel: Translating B to TLA+ for validation with TLC. Sci. Comput. Program. 131: 109-125 (2016)
-
Dominik Hansen, Michael Leuschel: Translating B to TLA + for Validation with TLC. ABZ 2014: 40-55
Diese Übersetzung hat einige Einschränkungen, und kann zB nicht mit zusammengesetzten Maschinen, DEFINITIONS oder Verfeinerung umgehen.
Minimalanforderungen
- Erweiterung von TLC4B um zusammengesetzte B Maschinen und DEFINITIONS zu unterstützen
Erweiterungen
- Unterstützung der Verfeinerung und von Event-B
- Empirische Auswertungen
Kontakt
Professor Michael LeuschelRaum 25.12.02.60 · michael.leuschel@hhu.de