Umfang

Dieses Thema kann im Umfang variiert werden, um als Bachelor-, Master- oder auch Teil einer Projektarbeit behandelt zu werden.

Empfohlene Vorkenntnisse

  • B oder Event-B Kenntnisse (z.B. durch Besuch der Veranstaltung “Sicherheitskritische Systeme”)

Problem

B0 ist eine low-level Teilmenge von B, in der nur noch wenige, sehr einfache Konstrukte erlaubt sind. Auf dieser Teilmenge arbeiten oft Code Generatoren, die solche Modelle z.B. nach C übersetzen.

Keiner dieser Code Generatoren ist bewiesen, was bedeutet, dass Bugs im Tool vorhanden sein können. Insbesondere für sicherheitskritische Anwendungen ist dies nicht sehr zufriedenstellend.

Gleichzeitig gibt es Model Checker für beispielsweise C. Die Forschungsfrage ist, ob sich Eigenschaften auf dem B Modell als Eigenschaft für einen low-level Model Checker, der auf generiertem Code arbeitet, ausdrücken lassen und sich diese Übersetzung automatisieren lässt. Dadurch hätte man zusätzliche Sicherheit, dass der generierte Code korrekt ist.

Minimalanforderungen

  • Auswahl eines passenden Model Checkers
  • Übersetzung von Eigenschaften

Erweiterungen

Die Teilmenge von B0 ist sehr eingeschränkt und eine händische Übersetzung ist oft sehr zeitintensiv. Daher arbeiten wir auch an einem Model Checker, der einige weitere Konstrukte mehr übersetzen kann.

Zusätzlich könnte man an Tooling von der anderen Richtung arbeiten: bestimmte Konstrukte kann man automatisiert clever eliminieren, sodass die Semantik beibehalten wird, aber man der B0-Teilmenge näher kommt. Beispielsweise kann man Mengen mit endlicher Basismenge in eine Reihe an Booleans umwandeln, die jeweils aussagen, ob eines der Elemente derzeit enthalten ist oder nicht.

Kontakt

Philipp Körner
Raum 25.12.02.56
p.koerner@hhu.de