Combining model-based development and formal verification of a complex ROS2 multi-robots system using Timed Rebeca

ROS2 is an increasingly popular middleware framework for developing robotic applications. A ROS2 application is composed of nodes that run concurrently, coordinate with each other through asynchronous interfaces, and can be deployed in a distributed manner. Rebeca is an actor-based language for modelling asynchronous and concurrent systems. Timed Rebeca adds timing features to deal with timing requirements of real-time systems. The similarities in concurrency and message-based asynchronous interactions of reactive nodes, and the ability of modelling timed behaviours justify using Timed Rebeca models to assist the development and verification of ROS2 applications. Model-based development and model-checking techniques allow faster prototyping and earlier detection of system errors before developing the entire real system. However, there are challenges in bridging the gap between continuous behaviours of robotic systems and discrete states in a model for automatic verification, and between complex robotic computations and inequivalent programming facilities in a modelling language like Timed Rebeca. We investigated the problem systematically and have succeeded in modelling a realistic multiple autonomous mobile robots (AMR) system using Timed Rebeca, creating corresponding ROS2 demo code, and showing the match between the model and the program. Based on experiments, we demonstrated the value of the model in development and automatic formal verification of correctness properties (target reachability, collision freedom, and deadlock freedom). Our model-checking results show that certain system problems are not always detected through simulation. The modelling principles, modelling and implementation techniques that are created and used in this work can be generalized for many other cases.