Formal Analysis and Verification of DDS in ROS2

Abstract

Robot Operating System(ROS) is widely used in the development of various service robots, which have high requirements in safety and reliability. Data distribution service(DDS) is deployed in ROS2 to implement the control of nodes and data distribution, which is very important for the operation of application on ROS2. In this paper, we focus on model abstraction, formal modeling and automatic verification for DDS in ROS2. A distributed model with interface parameters was established in PRISM. Properties such as security, liveness and priority of DDS in ROS2 were verified. The results show that the design satisfies these properties and high-priority messages can be sent and transmitted preferentially by the system. Due to the experiment result, we come up with a suggestion that the system will be better if its buffer can store six messages or more.