Model-based development and formal verification of a ROS2 multi-robot system using Timed Rebeca

Model-based development allows faster prototyping, earlier experimentation and validation of design intents. For a multi-agent system with complex asynchronous interactions and concurrency, model checking is a stronger and automated mechanism for verifying desired system properties. Timed Rebeca is an actor-based modelling language supporting both concurrent and time semantics, accompanied with a model-checking compiler. These capabilities allow using Timed Rebeca to correctly model ROS2 node topography, recurring physical signals, motion primitives and other timed and time-convertible behaviours. In this work we modelled a multiple autonomous mobile robots system in Timed Rebeca then developed corresponding ROS2 simulation code, ensured semantic synchronization between the model and the code, and set up experiments to use the model for revealing problems that do not always show up in simulation and verifying different properties (goal reachability, collision freedom, deadlock freedom, arrival times). The biggest challenges lie in abstracting complex information in robotics, bridging the gap between a discrete model and a continuous system and minimizing the state space, while maintaining the model's accuracy. We devised different discretization strategies for different kinds of information, identifying the 'enough' thresholds of abstraction, and applying efficient optimization techniques to boost computations to reduce model checking time. The benefits of formal verification are clear, however applying them in practice is difficult; our approach is a well explained, easy to understand, working solution in a realistic context.