Umfang

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

Empfohlene Vorkenntnisse

  • gute Kenntnisse in Java
  • grundlegende Kenntnisse in formalen Methoden, insbesondere der (Event)-B Modellierungssprache könnten hilfreich sein (z.B. durch Besuch der Veranstaltung “Sicherheitskritische Systeme”)

Problem

Event-B ist eine formale Modellierungssprache mit welcher wir mathematisch beweisbar korrekte Software entwickeln können. Dies ist insbesondere bei sicherheitskritischen Systemen erforderlich, um die Korrektheit von wichtigen Sicherheitseigenschaften zu überprüfen. Event-B verfolgt einen verfeinerungsbasierten Ansatz in welcher Anforderungen an einem sicherheitskritischen System schrittweise und hierarchisch in das Modell enkodiert werden. Für jeden Entwicklungsschritt wird eine Maschine erstellt welche die vorherige Maschine verfeinert, d.h., um zusätzliche Details ergänzt. Die zugehörigen Anforderungen inklusive der Sicherheitseigenschaften, die neu dazugekommen sind, sollten ebenfalls nach einem Entwicklungsschritt geprüft werden bevor man mit dem nächsten Schritt fortsetzt. Ebenso wird geprüft, ob der aktuelle Entwicklungsschritt mit dem Vorherigen konsistent ist.

Beispielsweise könnte man bei einem Aufzug zuerst die Bewegung (M0), danach die Türen (M1), und anschließend die Knöpfe (M2) modellieren. Es wäre allerdings auch möglich eine andere Reihenfolge für die Modellierung vorzunehmen. In diesem Beispiel könnte es sein, dass man nur Eigenschaften für die Türen überprüfen möchte, ohne die Aspekte der Bewegung und der Knöpfe zu betrachten. In vanilla Event-B ist die Verfeinerungshierarchie allerdings strikt, d.h., eine Maschine kann nur maximal eine andere Maschine verfeinern. Bezüglich unseres Beispiels verfeinert M1 bereits M0; es ist somit nicht mehr möglich dass M1 eine weitere Maschine verfeinert (in welcher nur die Türlogik, ohne die Bewegung modelliert sind).

Um dies zu ermöglichen, haben wir einen Ansatz vorgestellt in welcher es möglich ist weitere Abstraktionen zu erstellen:

  • Sebastian Stock, Fabian Vu, David Geleßus, Michael Leuschel, Atif Mashkoor, Alexander Egyed: Validation by Abstraction and Refinement. Proceedings ABZ, 2023

Aktuell ist allerdings viel manuelle Arbeit notwendig um den Ansatz umzusetzen. Im Rahmen dieser Arbeit soll ein Plugin für Rodin entwickelt werden, in welcher Abstraktionen als zusätzliche Parent-Maschinen in Event-B erstellt werden können. Die Rodin Plattform ist ein Eclipse-basiertes Tool mit welcher man Event-B Maschinen schreiben, beweisen, und model checken kann.

Minimalanforderung

  • Implementierung des Abstraktionsansatzes nach Stock et al.
  • Anbindung in Rodin als Plugin muss funktionieren

Erweiterungen

  • Erweiterung der Event-B Syntax um Abstraktionen
  • Generierung von neuen Beweisobligationen für Sicherstellung der Konsistenz zwischen Modell und Abstrahierung
  • ggf. Vergleich des Aufwandes zur manuellen Erstellung einer Abstraktion
  • ggf. Performanceanalyse

Kontakt


Fabian Vu
Raum 25.12.02.50
Fabian.Vu@hhu.de
Sebastian Stock
Sebastian.Stock@jku.at