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 Leuschel
Raum 25.12.02.60 · michael.leuschel@hhu.de