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

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

发送的数据块是整个数据流中第 k 个数据块,并初始化 count 为最大重传次数,N 表示整个数据流中数据块的个
数.此时,发布者由空闲状态转移到 Pub_datablock 发送数据块状态,并连续不断地发送之后的数据块.每个数据
块发送出去后,需要等待来自订阅者的确认信息.若在时间 timeout 之内收到确认信息 flag=true,则状态转移到
Datablock_Succ 数据块传输成功状态.在 Datablock_Succ 状态时,需要判断当前所传数据块是否是整个数据流
的终止数据块:若当前数据块为终止数据块,转换到 Success 成功状态,表示整个数据流传输成功,之后返回至
Idle 状态;否则,将回到 Pub_datablock 状态,接着发送下一个数据块.若在发送其中一个数据块时,在 timeout 时间
内没有收到来自订阅者的确认信息,则进入 Retransmit 重传状态.在最大重传次数内,可以允许重传当前数据块,
直到收到来自订阅者的确认信息.当重传次数用尽却没有发送完终止数据块或已经发送了终止数据块但没有
收到来自订阅者确认信息,则状态转移到 Fail 状态,表示数据流传输失败.在 Fail 状态时,发布者进入 Waitsync
状态,初始化同步信号 sync_signal 为 false,等待与订阅者同步;当 sync_signal 为 true 时,表示发布者与订阅者状
态同步,返回到 Idle 状态.

Fig.4 Probabilistic time automata model of data publish node
图 4 数据发布节点概率时间自动机模型
如图 5 所示为数据订阅节点的概率时间自动机模型.

Fig.5 Probabilistic time automata model of data subscription node
图 5 数据订阅节点概率时间自动机模型
数据订阅节 点模型的状 态空间包含 7 个状态 :S={Idle,Sub_datablock,Waitack,Retrans_wait,WaitSync,
Success,Data_state}.订阅者将要订阅的数据信息与发布者发布表中的数据信息进行匹配:若匹配成功,则相应