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

TL;DR

This paper demonstrates how to model and verify a multi-robot system using Timed Rebeca, addressing challenges in abstraction, discretization, and state space reduction to enable effective model-checking of complex ROS2-based systems.

Contribution

It introduces discretization strategies and optimization techniques for modeling continuous multi-robot systems in Timed Rebeca, facilitating formal verification of ROS2 multi-robot configurations.

Findings

Effective discretization thresholds identified for different information types

Model-checking performance improved through optimization techniques

Demonstrated round-trip engineering between models and implementation

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.