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 Leuschel
Raum 25.12.02.60 · michael.leuschel@hhu.de