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.