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

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

在面向数据流的 ROS2 数据分发服务的通信系统中,它允许部署一个或多个 DDS 域.同一域内的域参与者
通过匹配主题和 QoS 策略来发布订阅数据.在 DDS 通信系统中,发布者并不实际传输数据,而是通过创建和管
理数据写入者 DW i ,DW i 负责发布主题,并将数据发送给订阅该主题且 QoS 一致的订阅者.订阅者通过创建数据
读取者 DR j 订阅数据.ROS2 通信系统中,QoS 包括 DEADLINE,RELIABLITY,DURABILITY,HISTORY 策略.当
DW i 发布的主题与 DR j 订阅的主题且 QoS 策略一致时,就形成了数据发布订阅关系.若存在多个满足订阅主题
的 DW i ,选择其中一个符合对应 QoS 策略的 DW i 进行订阅,当 DW i 失效时,则可订阅其他的数据写入者中的数据.
因此,ROS2 通信系统解决了单点失效的问题.
2 基于 Prism 的系统建模

本文使用概率自动时间机来对 ROS2 面向数据流的数据分发服务进行形式建模.概率时间自动机是关于时
间和概率的有限自动机的扩展,它同时表示时间和概率,因此适合于在此模型中表示损失概率和时间延迟.根据
上节的系统描述,本节具体介绍系统中涉及到的主要模型形式化表示,并在 PRISM 概率模型检测器实现各模型
的概率时间自动机模型.

2.1 概率模型检测工具PRISM
概率时间自动机 [16] 是在时间自动机的基础上进行概率扩展,为实时系统在概率环境下的建模提供了一套
形式化的框架和机制.概率模型检测器 PRISM [17,18] 是由牛津大学开发研究的一个检测概率模型是否满足给定
时序逻辑属性的工具,它已被用于分析来自许多不同应用领域的系统,包括通信和多媒体协议、随机分布式算
法、安全协议、生物系统和许多其他系统.PRISM 可以构建和分析几种类型的概率模型:离散时间马尔可夫链
(DTMC)、连续时间马尔可夫链(CTMC)、马尔可夫决策过程(MDP)、概率自动机(PA)、概率时间自动机(PTA).
PRISM 首先分析模型的描述;然后构建概率模型的内部表示,计算模型可达状态空间并丢弃所有的不可达状态,
这意味着在建模系统中所有可能的组合集都可能会出现;接着解析逻辑规范,并通过归纳语法对模型应用适当
的模型检测算法进行验证.

2.2 系统在PRISM中的实现
根据系统描述中对 ROS2 数据分发服务的通信系统进行抽象,我们将系统形式化建模为数据发布节点概率
时间自动机模型、数据订阅节点概率时间自动机模型、全局数据空间概率时间自动机模型、通信信道模块概
率时间自动机模型.为了构建 ROS2 数据分发服务的通信系统模型,我们需要考虑以下情况:传输信道不可靠,即
数据在信道传输过程中可能会丢失,并且信道的数据丢包率为 P;数据传输时延不可忽略;数据被接受的次序与
其被发送的次序一致;在缓冲区溢出的情况下,新来的数据信息将会被直接丢弃.
2.2.1 数据发布节点和数据订阅节点概率时间自动机模型
在 DDS 中,节点既可以是数据发布者,也可以是数据订阅者.建模中,我们将节点分为数据发布节点和数据
订阅节点,分别建立概率时间自动机模型.图 4 所示为以数据流形式通信的发布节点概率时间自动机模型.DDS
作为 ROS2 的通信机制,通过数据流的方式进行数据的分发传输.数据流是一组有顺序、 有起始和终止的字节的
数据序列.在形式化模型中,我们可以将数据流看成是由多个数据块组成的数据序列,并用布尔类型的标记位对
每个数据块标识:fp 用来指示当前发送的数据块是否是起始的数据块,lp 指示当前发送的数据块是否是终止的
数据块,flag 用来判定数据块是否成功发送.flag 的初始值为 false,当数据块发送成功至订阅者,并收到来自订阅
者的确认信息,标记位 flag 替换成 true,代表当前数据块传输成功.然后发送下一个数据块,但在数据块连续发送
时,发布者在一段时间 timeout 内没有收到来自订阅者传来的确认信息,即 flag 值仍为 false,则中断连续数据块
的发送.发布者首先将时钟变量 t 重新设置为 0,并重传相应的丢失数据块.每个数据块重传的次数是有界的,最
大重传次数 conut 大小为 MAX.重传后,恢复连续发送.发布节点概率时间自动机模型的状态空间包含 8 个状
态:S={Idle,Pub_datablock,Waitack,Retransmit,Datablock_Succ,Success,Fail,Waitsync}.当没有数据发送时,发布者
的初始状态是空闲状态;当有数据需要发送时,将每一次通信的数据流划分成多个数据块,初始化 k 表示当前所