Problem Description

RoboRebeca is a framework to develop safe/correct codes for robotic applications. We suggest some modeling patterns to model robotic control systems using TRebeca language and propose an automatic code generation tool for converting Rebeca models to ROS. The models can be model checked/ analyzed/verified against desired properties in Afra, and then can be automatically transformed into correct ROS codes right there in Afra 3.0. Our toolset fully covers this chain for creating safe ROS codes for the robotic application. More details about this project is provided in this presentation: pptx

This work is continued in “Software for Safe Mobile Robots with ROS 2 and Rebeca” master thesis. This work focuses on a scenario in which mobile robots move from a starting position to the target position. Models of various ROS 2 components utilised in mobile robots are developed and both single- and multi- robot scenarios are verified.

Case Studies

  • The demo of Volvo Autonomous machines: [movie] (by Bahar Salmani).
  • Traffic Light Model: [zip] (by Bahar Salmani).
  • Train Controller Model: [zip] (by Bahar Salmani).
  • Kobuki Robot Controller Model: [zip] (by Bahar Salmani).
  • HXVolvo Model: [zip] (by Bahar Salmani).
  • Rebeca Models, Developed as a part of “Software for Safe Mobile Robots with ROS 2 and Rebeca” Master Thesis: [zip] (Kostiantyn Sharovarskyi).

Project Members

  • Marjan Sirjani (Principal Investigator)
  • Bahar Salmani
  • Giorgio Forcina
  • Ehsan Khamespanah