Umfang

Dieses Thema kann als Projektarbeit oder Masterarbeit bearbeitet werden.

Empfohlene Vorkenntnisse

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

Problem

BPMN (Business Process Model and Notation) ist eine Formalismus, mit dem in der Wirtschaftsinformatik häufig Geschäftsprozesse dokumentiert werden. Prinzipiell ähneln BPMN-Modelle einfachen Flowcharts, es gibt aber ein paar Erweiterungen.

Die Idee ist, dass man diese Modelle nach B übersetzt, um dann LTL-Formeln zu verifizieren. Ein Beispiel könnte sein, dass auf allen Wegen durch eine Fabrik Teile erst gebohrt werden, ehe versucht wird eine Schraube an diese Stelle reinzudrehen. Andere interessante Eigenschaften sind Deadlocks oder Livelocks.

Für die Arbeit würden echte Modelle zur Verfügung gestellt werden.

Minimalanforderungen

  • Übersetzung von BPMN Modellen nach B

Kontakt

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