Umfang

Dieses Thema kann als Teil einer Projektarbeit bearbeitet werden.

Empfohlene Vorkenntnisse

  • Kenntnisse der B Sprache sind erwünscht (zB. durch Besuch der Veranstaltung “Sicherheitskritische Systeme”)

Problem

In dieser Arbeit soll folgendes Problem in B oder Event-B modelliert werden:

fermatslibrary.com/s/the-parallel-climbers-puzzle Das Ziel wäre es

die Lösbarkeit des Problems formal zu beweisen Lösungen mit Modelchecking zu finden Lösungen bzw. Lösungsversuche mit Animation (unter Umständen BMotionStudio) zu visualisieren

Minimalanforderungen

  • funktionsfähiges (mit ProB ausführbares) B Modell

Erweiterungen (für Masterarbeit erforderlich)

  • Lösung mit Model Checking
  • formaler Beweis

Kontakt

Professor Michael Leuschel
Raum 25.12.02.60 · michael.leuschel@hhu.de