Pattern-based verification of ROS 2 applications using UPPAAL

Abstract This paper proposes an approach to pattern-based modeling and Uppaal -based verification for ROS 2 applications. The proposed verification focuses on callback execution latencies and buffer overflow. We propose formal model templates to model the execution of ROS 2 system components, created using a pattern-based approach. The model templates simplify the formal modeling of an ROS 2 application. Using Uppaal , we model in Uppaal timed automata, allowing the description of computation chains of ROS 2-based applications. Our focus is on execution behavior, including two versions of the mainline single-threaded executor of ROS 2. System traces generated using the formal models are validated in multiple experiments. Furthermore, we compare two approaches to modeling the execution of nodes that are typically the core units of computation of ROS 2. The first approach is a holistic approach to model ROS 2 applications, including communication and execution in computation chains. The second is an approach for individual nodes only, at a higher abstraction level. Additionally, we show the application of the verification by model checking in two ROS 2 system scenarios where we compare generated model traces to actual system executions. Overall, through formal modeling and verification, we showcase the potential for uncovering errors in the execution of distributed robotic systems.