Modellierung des Parallel Climbers Puzzles
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 LeuschelRaum 25.12.02.60 · michael.leuschel@hhu.de