You are required to read and agree to the below before accessing a full-text version of an article in the IDE article repository.

The full-text document you are about to access is subject to national and international copyright laws. In most cases (but not necessarily all) the consequence is that personal use is allowed given that the copyright owner is duly acknowledged and respected. All other use (typically) require an explicit permission (often in writing) by the copyright owner.

For the reports in this repository we specifically note that

  • the use of articles under IEEE copyright is governed by the IEEE copyright policy (available at
  • the use of articles under ACM copyright is governed by the ACM copyright policy (available at
  • technical reports and other articles issued by M‰lardalen University is free for personal use. For other use, the explicit consent of the authors is required
  • in other cases, please contact the copyright owner for detailed information

By accepting I agree to acknowledge and respect the rights of the copyright owner of the document I am about to access.

If you are in doubt, feel free to contact

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


Publication Type:

Conference/Workshop Paper


International Workshop on Reliability Engineering Methods for Autonomous Robots – REMARO 2024


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.


@inproceedings{Hong Trinh6940,
author = {Hiep Hong Trinh and Marjan Sirjani and Fereidoun Moradi and Antonio Cicchetti and Federico Ciccozzi},
title = {Combining model-based development and formal verification of a complex ROS2 multi-robots system using Timed Rebeca},
month = {June},
year = {2024},
booktitle = {International Workshop on Reliability Engineering Methods for Autonomous Robots – REMARO 2024},
url = {}