ProB Unterstützung für die CSSP
Umfang
Dieses Thema kann als Masterarbeit oder Projektarbeit bearbeitet werden.
Empfohlene Vorkenntnisse
- Kenntnisse der B Sprache (zB. durch Besuch der Veranstaltung “Sicherheitskritische Systeme”)
Problem
ProB ist ein Werkzeug zur Validierung formaler Spezifikationen. Die Clearsy Safety Platform baut auf B und Atelier-B auf und kann Code für eine neue Hardware für sicherheitskritische System entwickeln. Es gibt eine Reihe von Unterlagen fuur CSSP:
- https://github.com/CLEARSY/tutorial-ABZ-2021
- https://github.com/CLEARSY/CSSP-Programming-Handbook
In dem Projekt soll ProB verwendet werden um CSSP Projekte zu animieren und eventuell auch verifizieren.
Minimalanforderungen
- Unterstützung von ProB für CSSP Projekte
- Visualisierung der Ausgabe und des Zustands des Prozessors (zB mit VisB)
- empirische Analyse der Performance
Erweiterungen
- Anbindung innerhalb von Atelier-B
- Plugin für ProB2-UI
- Beweisführung mit Modelchecking oder dem ProB Disprover
Kontakt
Professor Michael LeuschelRaum 25.12.02.60 · michael.leuschel@hhu.de