<p>The verification of software applications built on top of the Robot Operating System 2 (ROS 2) is challenging due to the concurrent and physically distributed execution of callback functions. The organization of their execution influences application behavior and performance, because they interact not just with each other, but also with the underlying robotic and system components. Existing approaches lack a full-fledged analysis of the multi-threaded behavior of ROS 2 callbacks and their scheduling. Furthermore, these approaches do not consider the inner structure of callbacks and their organization. In this paper, we improve our model-driven DiNeROS framework using the base of Timed Petri nets (TPN). We integrate these aspects of ROS-based systems and enable the detection of potential defects in ROS applications, such as late, disordered, and deadlocking callbacks within and across nodes. We demonstrate our approach through two case studies involving a mobile industrial robotic arm, showing that the concurrent behavior and interaction of callbacks can be formally described and verified based on Timed Petri nets.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Enabling concurrency issue detection for ROS 2 using Timed Petri nets

  • Sebastian Ebert,
  • Ferdinand Auerswald,
  • Sebastian Götz,
  • Uwe Aßmann

摘要

The verification of software applications built on top of the Robot Operating System 2 (ROS 2) is challenging due to the concurrent and physically distributed execution of callback functions. The organization of their execution influences application behavior and performance, because they interact not just with each other, but also with the underlying robotic and system components. Existing approaches lack a full-fledged analysis of the multi-threaded behavior of ROS 2 callbacks and their scheduling. Furthermore, these approaches do not consider the inner structure of callbacks and their organization. In this paper, we improve our model-driven DiNeROS framework using the base of Timed Petri nets (TPN). We integrate these aspects of ROS-based systems and enable the detection of potential defects in ROS applications, such as late, disordered, and deadlocking callbacks within and across nodes. We demonstrate our approach through two case studies involving a mobile industrial robotic arm, showing that the concurrent behavior and interaction of callbacks can be formally described and verified based on Timed Petri nets.