Umfang

Dieses Thema kann als Projektarbeit oder Masterarbeit bearbeitet werden.

Empfohlene Vorkenntnisse

  • gute Prolog Kenntnisse (z.B. durch Besuch der Veranstaltung “Einführung in die logische Programmierung”)
  • Model Checking Kenntnisse könnten hilfreich
  • Kenntnisse der B Sprache könnten hilfreich sein (z.B. durch Besuch der Veranstaltung Sicherheitskritische Systeme)

Problem

ProB ist ein Validierungstool für Softwarespezifikationen insbesondere für die Formalismen, B, Event-B, TLA+, CSP, Alloy, etc. Das Tool selbst ist in der Programmiersprache Prolog implementiert und unterstützt Validierungstechniken wie etwa Animation und Model Checking. Basierend auf ProB gibt es die grafischen Nutzeroberflächen ProB Tcl/Tk und ProB2-UI. Letzeres ist in Java implementiert und enthält den Simulator SimB. Mithilfe von SimB kann man formale Modelle durch Annotation von Events mit Timing und probabilistischen Eigenschaften simulieren.

Für die Modellierung, Simulation, und Verifikation von Robotersysteme werden unter anderem die Formalismen RoboChart und RoboSim verwendet, welche im Rahmen des RoboStar Projektes entstanden sind. RoboChart und RoboSim lassen sich ebenfalls in andere Formalismen, wie etwa CSP, tock-CSP und probabilistic timed automaton in PRISM übersetzen.

Die Aufgabe dieser Arbeit besteht darin ProB so zu erweitern, dass man RoboChart oder RoboSim Modelle animieren, model checken, und simulieren kann. Hierzu ist es auch notwendig zu untersuchen, welche Aspekte von RoboChart bzw. RoboSim durch die Übersetzung nach CSP, tock-CSP und PRISM abgedeckt werden. Anschließend soll eine geeignete Lösung gefunden und implementiert werden.

Minimalanforderung:

  • funktionsfähige Erweiterung von ProB für Robotersystemen in Robochart/RoboSim
  • Animation, Model Checking, und Simulation in ProB (bzw. SimB) muss möglich sein
  • Untersuchung welche Aspekte durch die Übrsetzung von RoboChart/RoboSim nach CSP, tock-CSP und PRISM abgedeckt werden
  • Untersuchung inwiefern die nach CSP übersetzten RoboChart/RoboSim Modelle bereits in ProB unterstützt werden

Erweiterung:

  • empirische Auswertung der Performance

Kontakt

Fabian Vu
Raum 25.12.02.50 · fabian.vu@hhu.de