Formal Analysis and Verification of DDS in ROS2
Formal Analysis and Verification of DDS in ROS2
复制标题
ROS2中DDS的形式化分析与验证
DOI：
10.1109/memcod.2018.8556970
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Jie Zhang
中科院分区：
文献类型：
--
作者：
Yanan Liu;Yong Guan;Xiaojuan Li;Rui Wang;Jie Zhang
机器人操作系统（Robot Operating System，ROS）广泛应用于各种服务机器人的开发中，这些机器人对安全性和可靠性要求很高。在ROS2中部署了数据分发服务（DDS）来实现节点控制和数据分发，这对于应用程序在ROS2上的运行至关重要。在本文中，我们专注于模型抽象，形式化建模和自动验证的DDS在ROS2。在PRISM中建立了一个带界面参数的分布式模型。在ROS2中验证了DDS的安全性、活性和优先级等特性。结果表明，该设计满足这些性质，系统可以优先发送和传输高优先级的消息。根据实验结果，我们提出了一个建议，如果系统的缓冲区可以存储六个或更多的消息，将是更好的。
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.