https://www.mdu.se/

Robot operating system 2 (ROS 2) is increasingly popular both in research and commercial robotic systems. ROS 2 is designed to allow real-time execution and data communication, enabling rapid prototyping and deployment of robotic systems. In order to predict and calculate execution times in ROS 2, one needs to analyze its internal scheduler, called executor. The executor has been updated in various distributions of ROS 2, which is shown to impact significantly the periodic execution invoked by the underlying operating system's timers, potentially causing unexpected latencies. To expose the mentioned impact due to executor differences, in this paper, we present an experimental evaluation of the execution behavior of ROS 2's schedulable entities, namely callbacks, among the existing versions of the executor. We visualize the differences of callback execution order via simulation, and we create design-level scenarios that impact the execution of periodically scheduled callbacks, negatively. Moreover, we show how such negative impact can be mitigated by using multi-threaded executors. Finally, we illustrate the observed behavior on a real-world centralized multi-agent robot system. Our work aims to raise awareness within the ROS 2 developer community, regarding possible problems of timer blocking, and propose a mitigation solution of the latter.

This paper proposes a pattern-based modeling and Uppaal-based verification of latencies and buffer overflow in distributed robotic systems that use ROS 2. We apply pattern-based modeling to simplify the construction of formal models for ROS 2 systems. Specifically, we propose Timed Automata templates for modeling callbacks in Uppaal, including all versions of the single-threaded executor in ROS 2. Furthermore, we demonstrate the differences in callback scheduling and potential errors in various versions of ROS 2 through experiments and model checking. Our formal models of ROS 2 systems are validated in experiments, as the behavior of ROS 2 presented in the experiments is also exposed by the execution traces of our formal models. Moreover, model checking can reveal potential errors that are missed in the experiments. The paper demonstrates the application of pattern-based modeling and verification in distributed robotic systems, showcasing its potential in ensuring system correctness and uncovering potential errors.

In this paper, we propose a formal modeling approach in uppaal to simulate and verify multi-threaded robotics middleware execution based on ROS 2. In the modeling process, we consider middleware-specific scheduling by creating formal models that simulate the execution behavior of a ROS 2-based system. Furthermore, we show how to model potential underlying operating system's influences on execution by modeling reservation servers. We propose timed automata templates to model the multi-threaded execution of ROS 2 systems and the reservations of the underlying operating system in uppaal.We show how to utilize the created templates to simulate a ROS 2 application. We demonstrate the application of the formal models and model checking in various ROS 2 experiments. Furthermore, we validate the created models by comparing the observed execution traces in experiments on ROS 2 systems and the simulated traces of our models.Overall, this paper showcases the application and usability of model-based verification of distributed middleware applications, including internal scheduling and influences of underlying operating system actions.

To simplify the formal verification of ROS 2-based applications, in this paper, we propose a novel approach to the automation of their model-based verification using model-driven engineering techniques. We propose a methodology starting with ROS 2 execution traces, generated by ROS2_tracing and using models and model transformations in Eclipse to automatically initialize pre-defined formal model templates in UPPAAL, with system parameters. While the methodology targets the simplification of formal verification for robotics developers as users, the implementation is at an early stage and the toolchain is not fully implemented and evaluated. Hence, this paper targets tool developers and researchers to give a first overview of the underlying idea of automating ROS 2 verification.

Hence, we propose a toolchain that supports verification of implemented and conceptual ROS 2 systems, as well as iterative verification of timing and scheduling parameters. We propose using four different model representations, based on the ROS2_tracing output and self-designed Eclipse Ecore metamodels to model the system from a structural and verification perspective. The different model representations allow traceability throughout the modeling and verification process.Last, an initial proof of concept is implemented containing the core elements of the proposed toolchain and validated given a small ROS 2 system.