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

1826 Journal of Software 软件学报 Vol.32, No.6, June 2021

表中,若存在主题信息及其对应的 QoS 参数信息一致的发布者,则匹配成功.若有多个发布者满足条件,则按照
一定策略选取一个作为订阅的对象.若不存在主题信息与 QoS 参数一致的发布者,则订阅失败,将订阅失败记录
添加到订阅失败表 Sub_fail_table 中.
2.2.3 通信信道概率时间自动机模型
通信信道模块主要用于发布者订阅者之间的数据传输,在数据流传输过程中,由于信道是不可靠的,可能会
发生数据丢失,丢包率为 p[i],在此概率下,数据会发生重传;数据成功传输的概率为 1−p[i],变量 N 为整个数据流
中数据块的数量,k 表示数据发布者当前正在传输的数据块是数据流中的第 k 个数据块,m 表示数据订阅者当前
正在接收的数据块是数据流中的第 m 个数据块.图 7 表示通信信道模块概率时间自动机模型.通信信道模型的
状态空间包含 4 个状态:S={Idle,Transmit,Success,Fail}.当发布订阅节点匹配成功后,数据发布者将会将数据发
送给主题信息与 QoS 参数一致的订阅者.当发送的数据块没有达到 N 时,说明仍有没有发送的数据块,则通信信
道由空闲状态转移到 Transmit 状态,发送当前的数据块.如果在时钟变量 timeout 内,订阅者收到来自发布者发送
的数据块以及发布者收到来自订阅者的确认信息 flag=true,则说明当前数据块传输成功,然后状态转移到 Idle,
等待传输下一个数据块;否则说明数据传输失败,状态转移至 Fail 状态,重置时钟变量,回到 Idle 状态等待该数据
块的重传.

Fig.7 Probabilistic time automata moduleof communication channel
图 7 通信信道概率时间自动机

3 属性抽象与形式化表达

为了验证系统功能的正确性,本文抽取 3 个关键属性.属性的抽象表示如下:
(1) 安全性
对于面向数据流的 ROS2 通信系统,如果系统在某个时刻进入死锁状态,则系统不能正常运行.在 PRISM 中,
验证系统无死锁的属性可以表示为:“init”=>P≥1[true & !“deadlock”].
(2) 可靠性
不同的应用对 DDS 性能的要求不同.DDS 提供了 Best-Effort(高效传输),Reliable(可靠传输)两种传输方式,
以满足不同应用的需要.通过 QoS 属性的配置,可以对数据传输方式进行选择.可靠传输模式对于 DDS 来说,它
应该在不同的条件下完成规定大小数据的分发.
属性 R=?[C≤t]为 PRISM 中的累计奖励公式,主要是计算在时间 t 内,数据发布订阅成功传输的累计数据量.
在实验中,我们使用计算时间 t 内数据成功传输的数据量的属性,验证在 QoS 为可靠传输时的数据传输情况.在
模型中使用了两个参数 N,P,分别表示传输数据的数据量、信道的数据丢包率,如图 8 所示.实验中设置整个数
据流中数据块块数 N 为 20,验证在不同数据丢包率 P 的情况下,完成数据传输所对应的不同的奖励期望值 R 是
多少.从实验结果可以看出:在 QoS 为可靠传输方式的情况下,随着数据丢包率的变化,每个曲线都很接近,并最
终显示都可以完成规定数据流大小的数据传输,即奖励期望值 R 与数据块块数 N 相等都为 20.验证了 DDS 在
QoS 为可靠传输下数据传输的可靠性.这表明:DDS 在可靠传输模式时,因其较好的数据重传机制,发送数据成