Pattern-based verification of buffer sizes and callback latencies of ROS 2 nodes using UPPAAL

Abstract: This paper proposes a pattern-based modeling and \uppaal-based verification of latencies and buffer overflow in distributed robotic systems. 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 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 overlooked errors.

@inproceedings{ref:dust2023pattern,

  title={Pattern-Based Verification of ROS 2 Nodes Using UPPAAL},

  author={Dust, Lukas and Gu, Rong and Seceleanu, Cristina and Ekstr{\"o}m, Mikael and Mubeen, Saad},

  booktitle={International Conference on Formal Methods for Industrial Critical Systems},

  pages={57--75},

  year={2023},

  organization={Springer}

}

Keywords: Robot Operating System 2, Pattern-Based Modeling, Model Checking

Contact: lukas(dot)dust(at)mdu.se

Selected ROS 2 component features and their abstraction in the UTA model