Modelling and Model-Checking a ROS2 Multi-Robot System using Timed Rebeca

TL;DR

The paper addresses the challenge of verifying safety and liveness in ROS2-based multi-robot systems by building a holistic model in Timed Rebeca and aligning it with ROS2 code. It demonstrates a round-trip engineering flow, employing discretization strategies to bridge continuous robotic dynamics with a finite-state verifier and using model-checking to validate properties such as collision freedom and reachability. Key contributions include a Timed Rebeca model of a multi-robot architecture, discretization techniques for map, motion, and sensing, optimization methods to speed verification, and a human-like congestion avoidance algorithm, all validated against ROS2 simulations. The work advances model-based development for robotics by providing a concrete, verifiable framework and outlining future steps toward automatic generation of verification artifacts and tighter integration with real-time implementations.

Abstract

Model-based development enables quicker prototyping, earlier experimentation and validation of design intents. For a multi-agent system with complex asynchronous interactions and concurrency, formal verification, model-checking in particular, offers an automated mechanism for verifying desired properties. Timed Rebeca is an actor-based modelling language supporting reactive, concurrent and time semantics, accompanied with a model-checking compiler. These capabilities allow using Timed Rebeca to correctly model ROS2 node topographies, recurring physical signals, motion primitives and other timed and time-convertible behaviors. The biggest challenges in modelling and verifying a multi-robot system lie in abstracting complex information, bridging the gap between a discrete model and a continuous system and compacting the state space, while maintaining the model's accuracy. We develop different discretization strategies for different kinds of information, identifying the 'enough' thresholds of abstraction, and applying efficient optimization techniques to boost computations. With this work we demonstrate how to use models to design and verify a multi-robot system, how to discretely model a continuous system to do model-checking efficiently, and the round-trip engineering flow between the model and the implementation. The released Rebeca and ROS2 codes can serve as a foundation for modelling multiple autonomous robots systems.

Figures (15)

• Figure 1: A ROS2 node graph (source: docs.ros.org).
• Figure 2: Modelling laser scan events
• Figure 3: Collision check based on intersection of shadows
• Figure 4: Blocking obstacles
• Figure 5: Sequence diagram of map server–robot interactions