Modeling and Verification of ROS 2 Callback Concurrency Using UPPAAL Model Checker

Robot Operating System 2 (ROS 2) has become the de facto standard middleware for developing robotic applications. The execution of ROS 2 applications heavily relies on callback functions, which execute concurrently within a ROS 2 node. The concurrency of these callbacks significantly impacts application behavior, yet its thorough analysis remains challenging due to the complex interaction of multiple system components. To address the need for an exhaustive analysis of ROS 2 callback concurrency behavior, this paper presents a novel and practical approach for modeling and verification using the UPPAAL model checker. We introduce a set of callback concurrency models, incorporating key elements such as callbacks, callback groups, threads, and executors, alongside model checking queries. Furthermore, we present a tool that automates the generation of UPPAAL model code from high-level specifications, offering a streamlined solution for practitioners. To demonstrate the validity and effectiveness of our approach, we model three representative cases of callback concurrency configurations in ROS 2 and verify four notable concurrency behaviors. Our results accurately capture callback concurrency behavior compared to the execution logs of real ROS 2 applications, making the proposed models and queries reusable and extendible for analyzing ROS 2. The verification reports on recent ROS 2 versions also reveal issues such as callback starvation and unfairly overloaded threads, providing valuable insights for developers and practitioners working with ROS 2 in the industry.