Page 245 - 《软件学报》2021年第6期

芦倩 等:面向数据流的 ROS2 数据分发服务形式建模与分析 1819

probability model test and analysis, validates real-time and reliability of the ROS2 system. Firstly, a data flow oriented ROS2 data
distribution service system of communication formal validation framework is put forward, and the communication system module
probabilistic timed automata model is set up. Secondly, probabilistic model detector PRISM is used to verify the real-time and reliability
of ROS2 data flow oriented data distribution service through parameter analysis of data loss rate and system response time. Finally, based
on retransmission mechanism, quality of service (QoS) strategy analysis, through the set up and adjust service quality parameters,
different data requirements and quantitative performance analysis of transmission mode are achieved, providing the reference for
application designers based on ROS2 and distributed data distribution service based on the data flow of formal modeling, validation, and
quantitative performance analysis.
Key words: ROS2; data distribution service; QoS; probabilistic timed automata; PRISM; formal modeling and analysis

ROS 是开源的元操作系统,已广泛用于机器人软件研发.随着机器人相关技术的日益普及,对机器人应用的
要求也在相应地提高,因此需要对机器人操作系统进行分析,使系统对外界的信号等信息及时地作出相应的动
作.但是,ROS 机器人操作系统存在两个主要问题:通信延迟高和可靠性差.ROS 的性能受到其高延迟序列化方
[1]
法和与 TCP/UDP 的套接字通信的限制,在消息传递过程中会带来多次内存复制 .因此,ROS 系统实时性不高,
不能直接应用于实时控制和关键任务应用.并且 ROS1 的通信系统基于 TCPROS/UDPROS,强依赖于主节点的
处理,一旦主节点出现故障,系统可靠性将会受到很大的影响,在一定程度上限制了 ROS 的实际应用.
ROS2 在 ROS 的基础上改进应用了众多新技术,带来了整体架构的颠覆.为了改善 ROS1 实时性、可靠性
问题,ROS2 采用面向数据流的数据分发服务(data distribution service,简称 DDS)作为其通信机制.DDS 是对象管
理组织提出的一种以数据为中心的新一代分布式系统数据规范,它允许使用发布-订阅机制进行可靠和实时的
数据收集和交付,支持节点的动态发现、基于主题的数据分发和数据流的时空解耦.因此,该数据规范保证了数
据分发的实时性与可靠性,并且由于其灵活的配置方法和其可扩展性而广泛应用于实时分布式系统中.与其他
[2]
[3]
发布订阅中间件相比,DDS 的一个主要特征是具有极其丰富的 QoS 支持 .QoS 策略提供了数据传输的保证 .
系统设计者可以根据这些 QoS 参数,基于特定的要求和可用性来构建分布式应用.面向数据流的 ROS2 数据分
发服务机制相对于以主节点为中心的基于消息的数据分发机制,能较好地满足分布式节点间数据通信的实时
性、提高数据传输效率,因此擅长处理数量庞大和复杂多变的数据.通过控制 QoS 参数,可以将对更新速率、可
靠性和带宽控制等有不同要求的模块很好地集成到系统中.但是随着系统内部数据交互频繁,同时,随着系统规
模的扩大,系统中发送者和订阅者的数量、数据类型和 QoS 需求也随之增加,系统性能会急剧下降,并且不同的
应用对 DDS 性能的要求有不同的差别.这些问题都会给数据分发带来严峻的考验,给设计造成隐患.所以在系
统开发早期应该对其进行分析,但是使用传统的测试和仿真方法,无法对系统模型进行完备的验证.形式化方法
[4]
运用数学和逻辑的方法描述和验证系统.形式化验证 与传统的验证方法相比,以形式化方法为基础的工具进
行辅助设计和验证,对提高系统的可信度有很大帮助.并且能够对指定描述的所有可能的情况进行验证,有效地
克服了模拟验证的不足.概率模型检测结合了概率分析和通用的模型检测技术,适用于验证非确定的系统,并可
实现量化分析.因此,我们使用形式化验证中的概率模型检测的方法分析系统的正确性,基于形式化模型进一步
对系统性能进行参数化分析,从而给系统设计人员和 ROS 程序开发人员提供有价值的参考.
[5]
已有学者对有关 DDS 的形式化验证问题进行了研究.He 等人 最先基于概率时间自动机对发布订阅系统
[6]
[7]
进行了形式化建模.Liu 等人 验证了 DDS 在 ROS2 中的活性.Yin 等人 使用通信顺序进程(CSP)对实时发布订
阅协议(RTPS)中的多个模块中组件进行了建模,通过使用模型检测工具 PAT 验证了不发散性、确认机制、数据
一致性等属性.上述工作都对数据分发机制进行了形式化建模,但大多数是对基于消息的数据分发机制进行建
模,没有对 QoS 策略进行形式描述,缺少对系统的性能的分析.QoS 是控制了各方面与底层的通信机制,是用于解
决延迟和阻塞的传输控制策略.在关键和分布式系统运行时,需要保证可靠性并且满足所需的性能.调整 QoS 参
数可以满足不同场景的数据应用需求,对系统实时性可靠性有至关重要的影响.而对系统 QoS 服务质量分析的
[8]
国内外研究中,Maruyama 等人 阐明了 ROS1 和 ROS2 在各种情况下的数据传输性能.从延迟、吞吐量、线程
数和内存消耗对比 ROS1 与 ROS2 的性能.QoS 自适应方法是基于发布/订阅中间件开发实时系统的一种有效的
方法,在动态环境中开发大型实时分布式系统时,其重要性日益提高.当在众多异构实体之间传播大量数据时,