Ad Hoc网络中有限重传协议的建模与分析

陈立斌, 文 英

(1. 湖南理工学院 计算机学院, 湖南 岳阳 414006; 中国移动集团广西有限公司 南宁分公司, 南宁 530028)

Ad Hoc网络中有限重传协议的建模与分析

陈立斌1, 文 英2

(1. 湖南理工学院 计算机学院, 湖南 岳阳 414006; 中国移动集团广西有限公司 南宁分公司, 南宁 530028)

在节点不断移动、拓扑动态变化、带宽受到限制的Ad Hoc网络中, 节点间的通信会受到收发节点间相邻概率、信道质量等因素的影响. 本文应用概率模型检测技术, 基于有限状态机和马尔可夫决策过程, 对Ad Hoc网络环境中的有限重传协议进行建模, 并使用PRISM工具量化分析了节点间信道质量、文件的分组数和重传的最大次数对网络通信的影响, 验证了协议相关性质, 分析结果有助于根据网络实际情况设置协议各参数, 从而提高网络性能.

有限重传协议; Ad Hoc网络; 概率模型检测; PRISM

Abstract:In Ad Hoc network, mobile node with limited bandwidth moves frequently and topology changes dynamically. The communication between nodes is dynamically affected by many factors, such as the neighbor probability, channel quality and so on. Based on Probabilistic Model Checking, the Bounded Retransmission Protocol (BRP) in Ad Hoc Network is modeled. Then the influence of channel quality, the number of data frames and the maximum number of retransmission on the communication are analyzed with Probabilistic Model Checking tool-PRISM. The analysis results are helpful to adjust various parameters of protocol according to the different situation in order to improve the performance of the network.

Key words:bounded retransmission protocol; Ad Hoc network; probabilistic model checking; PRISM

引言

有限重传协议[1,2](Bounded Retransmission Protocol, BRP)是一种用于不可靠通信线路上传送大型数据包的数据链路层协议, 基于交错位协议(Alternating Bit Protocol, ABP), 并允许以块的形式(如文件的某一部分)进行有限次重传, 采用了有确认的停等策略, 类似于ARQ机制: 发送方在发送一帧数据后, 等待对方应答; 当接收方收到一个正确的数据帧后, 向发送方发送一个确认帧; 当发送方收到此确认帧后才能发送一个新的数据帧. 同时, 收发双方都使用了计时器以保证其实时性, 并限定了最大重传次数, 其流程类似于X.25协议中的LAPB链路控制过程[3]. 文献[4]应用基于进程代数的μCRL对BRP进行了形式化规约和分析, 并使用定理证明器Coq对协议性质进行了验证. 文献[5]使用UPPAL和SPIN工具对BRP及协议相关性质进行了验证. 上述文献均侧重于对协议性质的验证, 缺乏对协议相关参数的量化分析.

在节点不断移动、拓扑动态变化、带宽受到限制的Ad Hoc网络中, 节点间的通信受到收发节点间相邻概率、信道质量等因素的影响. BRP在Ad Hoc网络环境下的研究较少. 基于此, 本文应用概率模型检测技术,对Ad Hoc网络环境中的BRP进行了建模, 通过一定的概率来描述信道的不可靠性, 并用PRISM[6]工具量化分析了节点间信道质量、文件的分组数和重传的最大次数对网络通信的影响, 验证了协议相关性质, 分析结果有助于根据网络实际情况设置协议各参数, 从而提高网络性能.

1 Ad Hoc网络中有限重传协议的建模

1.1 协议描述

BRP由发送方S (Sender)、接收方R (Receiver)以及两个按照FIFO方式处理数据的不可靠信道M (用于发送数据帧)和A (用于发送确认帧)组成, 其原理如图1所示, 其中REQ、CONF、E、F、G、H和IND均为通信端口, t1和t2分别为发送方和接收方的定时器.

BRP提供了发送方的请求服务、确认服务, 接收方的指示服务这三类服务原语, 分别表示如下:

(1) REQ(s)

请求服务负责以独立数据帧的形式来发送一定长度的数据.

(2) CONF(c) (c∈{C_OK, C_NOK, C_DK})

确认服务负责将请求服务的结果告知发送方.

C_OK: 成功发送请求信息;

C_NOK: 未能完全发送请求信息;

C_DK: 不能确定是否处理完请求信息. 仅当已发送最后一帧但没有收到确认帧时才会出现这一情况.

(3) IND(d, i) (d是一个数据, i∈{I_FST, I_INC, I_OK})

指示服务负责判断数据帧的序号, 并将新的数据帧发送给接收方.

I_FST: 收到的数据帧为第一帧;

I_INC: 收到的数据帧为中间帧;

I_OK: 收到的数据帧为最后一帧, 此时文件块已传送完毕.

(4) IND_NOT_OK

当通信发生故障时, 接收方只收到部分消息, 此服务原语则负责将故障情况告知发送方.

在此协议中, 将文件划分为N ( N ＞2)块, N = 1时协议等价于ABP. 初始时重传计数器为0, 其最大值为MAX; 消息经信道M和A传送后, 以一定的概率正确到达或发生丢失. 信道M所发送的数据帧由三个比特位和数据块组成, 其格式为(first, last, toggle, data); 相应地, 信道A所发送的确认帧格式为(first, last, toggle), 可以将其看作是数据帧除去数据后的头部信息. 其中first和last是布尔变量, 取1时(true)分别表示此帧为所传送文件的第一帧和最后一帧; toggle是布尔变量, 为帧标志位, 接收方保存当前toggle值用于区别后续数据帧以避免重复, 初始值为0; data为数据. 例如, 第一帧可表示为(1, 0, 0, d1).

图1 BRP

在没有帧丢失的正常通信情况下, 协议主要流程如下: 假设接收方R在发送传送文件数据d1…dN的请求REQ(d1…dN)后启动定时器t2, 发送方S接收到此请求, 则通过端口E发送帧(1, 0, 0, d1), 并启动定时器t1. 信道M通过端口F将此帧传送给R. 若在t2超时前收到此帧, R通过IND端口发送IND(d1, I_FST), 并在端口G处发送确认帧(1,0,0), 保存此帧中的toggle位后重置定时器t2, 此确认帧通过信道A到达端口H.在t1超时之前收到确认后, S将发送第二个数据帧(0,0,1,d2), 此帧将前一数据帧中toggle这一标志位置反,即为1, 并重置定时器t1; 若发生超时, 重发此帧, 并将重传计数器加1(若重传计数器超过其最大值MAX, 则文件传送失败). 类似地, 在t2超时之前收到第二帧后, 接收方发送IND(d2, I_INC)和确认帧(0, 0, 1), 保存此帧中toggle位后重置定时器. 重复此过程, 直到最后一帧发送完毕, 此时数据帧为(0,1,¬toggleN-1,dN), 接收方发送IND(dN, I_OK)和确认帧(0,1,¬toggleN-1), 并报告完成文件传送和确认.然后, 发送方将发送CONF(C_OK), 报告文件传送成功.

1.2 协议分析与建模

在通信过程中, 若数据帧或确认帧发生丢失, 从发送方的角度进行分析如下. 当发送方S发送数据帧时, 启动定时器t1, 等待接收方R的确认. 若在t1超时前收到确认, 则重置定时器并发送新的数据帧; 若t1超时且没收到确认, 则重传帧; 若已经达到最大重传次数, 发送方则放弃传送. 若在传送最后一个数据帧时发生故障, 则调用CONF(C_DK)这一确认服务, 判断是最后一个数据帧丢失以至没有收到, 还是此帧的确认帧丢失; 否则若在传送过程中发生故障, 则调用CONF(C_NOK)确认文件传送失败.

下面从接收方的角度来分析帧丢失的情况, 在此假定第一个数据帧不会发生丢失. 当收到一个数据帧时, 接收方对此帧进行确认. 此数据帧中toggle位与前一帧中toggle位取值不同时, 则此帧为新帧. 发送确认后启动计时器t2, 并进入等待状态. 若t2超时且没有收到数据帧, 则调用IND_NOT_OK. 仅当发送方终止传送时, 才会发生超时. 在通信中断一定时间后, S和R将重新同步启动. 考虑信道传输延时(Channel Delay, CD), 从上述分析中可知, t2＞ max (t1+ CD), 这样才能保证R能有足够时间对接收的数据帧进行处理.

在Ad Hoc网络中, 节点间的通信受到收发节点间相邻概率、信道质量等因素的影响. 为了便于建模,对Ad Hoc网络及协议进行如下假设:

(1)网络面积为A, A = 1000×1000(m2), 移动节点随机分布其中, 并独立地自由移动;

(2)节点的有效传输半径为R, R = 250(m), 处于有效传输范围内的节点间可以直接通信. 在此不考虑噪声的影响.

(3)信道M丢失数据帧的概率为1-q1, 信道A丢失确认帧的概率为1-q2.

由上述假设可知, 收发节点处于有效传输范围内的概率为πR2/A. 根据BRP的执行流程, 可以得出协议中各组件的有限状态机如下.

图2 BRP中发送方S的有限状态机

BRP中发送方S的有限状态机如图2所示. 其中idle为空闲状态, next_frame为发送新数据帧状态, wait_ack为等待确认帧状态, retransmit为重传数据帧状态, success为发送成功状态, error为发送失败状态, wait_sync为等待同步状态.

初始时S处于idle状态, 当收到发送信息请求时, 就进入next_frame状态开始发送新的数据帧, 同时启动定时器. 发送之后进入wait_ack状态, 等待R的确认信息. 若在超时之前收到确认, 则发送成功进入success状态, 接着发送下一个数据帧, 重复此过程, 若发送完毕就进入idle状态; 若超时且没有收到确认帧, 则进入restransmit状态进行重发; 若重发次数超过最大值MAX, 则放弃传送进入error状态, 同步之后进入idle状态.

BRP中接收方R的有限状态机如图3所示. 其中new_file为等待接收数据帧状态, fst_safe为判断是否为第一个数据帧的状态, frame_received为数据帧接收状态, frame_reported为报告情况状态, idle为空状态, resync为同步状态.

图3 BRP中接收方R的有限状态机

初始时R处于new_file状态, 接收数据帧后相继进入fst_safe和frame_received状态. 此数据帧可能是第一帧、中间帧或最后一帧, 因而R对此进行判断进入frame_reported状态, 并将结果输出到IND端口. 然后将确认信息反馈给S, 进入idle状态,同时判断所接收的前一数据帧是否为文件最后一帧并记录其标志位. 若没有接收完毕, 继续等待接收, 并根据标志位判断是否为重复帧. 如接收的数据帧是最后一个, 则此次文件传送完成, 等待同步之后, 可以再次开始新的文件传送; 若长时间等待后仍没收到S方响应, 则报告文件传送失败, 等待同步后重新接收.

图4 信道M的概率有限状态机

图5 信道A的概率有限状态机

图6 Checker的有限状态机

信道M、A只有三个状态, 即空闲状态idle、发送状态send和丢弃状态lost. 信道M和A的成功发送概率分别是q1和q2, 即丢弃信息的概率分别为1-q1和1-q2. 新文件检测器(Checker)则用于启动新文件的传送.

2 协议相关参数及部分代码

为了描述协议中各组件的非确定的概率行为, 将其建模为马尔可夫决策过程(Markov Decision Processes, MDP), 每一组件用PRISM的一个模块表示, 协议相关参数及部分代码如下:

3 结果分析

使用PRISM对BRP进行验证, 结果分析如下:

(1) 发送方报告不确定文件是否成功传送而接收方得到文件完整信息的最大概率

图7 参数MAX、N、q1、q2中其一变化而其它三个不变时的最大概率

该性质可规约为Pmax=?[true U (srep=NOK & rrep=OK & recv=true)], 结果如图7所示. 发送方报告不确定文件是否成功传送而接收方得到文件完整信息的状态是不可达的, 其最大概率始终是0, 不随参数MAX、N、q1、q2的变化而变化. 同理, 发送方报告文件传送成功而接收方没有得到文件完整信息的概率的最大概率也为0. 由此可知, 协议具有安全性. 此外, 若接收节点不可靠(如一些恶意节点, 正确接收却报告错误等), 可推知会破坏协议安全性, 在此不再作分析.

(2)发送方报告文件传送成功的最大概率

图8 发送方报告文件传送成功的最大概率

该性质可规约为Pmax=?[true U (srep=OK & T=true)]. 同理, 发送方报告文件传送失败这一性质可规约为Pmax=?[ true U (s=error & T=true)]. 由图8可知, 发送方报告传送成功的最大概率随着MAX、q1、q2的增大而增大, 随N的增大而减少. 这是因为重传的次数越大, 信道的传输质量越好, 数据传送成功的概率则越大; 而一个文件的分组数N增大时, 其传输效率降低, 因而不宜过大.

(3)发送方报告不确定文件是否成功传送的概率

图9 发送方报告不确定文件是否成功传送的最大概率

该性质可规约为Pmax=?[true U (s=error & T=true & srep=DK)], 这一性质描述了信道质量对协议性能的影响. 如图9所示, 发送方报告不确定文件是否成功传送的最大概率随着MAX、N的增大总体趋于减小,随着q1、q2的增大而增大.

(4)接收方不能接收任何数据而发送方仍试图发送数据的最大概率

图10 接收方不能接收任何数据而发送方仍试图发送数据的最大概率

该性质可规约为Pmax=?[true U ( srep!=0 & T=true & recv=false)], 这一性质描述了协议正确完成的情况.由图10可知, 接收方不能接收任何数据而发送方仍试图发送数据的最大概率随着MAX的值增大而减少,即协议正确完成的概率越高, 具有一定的活性; 随着q1、q2的增大而减小, 且不随N的变化而变化.

[1] Helmink L, Sellink M P A, Vaandrager F W.Proof Checking a Data Link Protocol[J]. In Proceedings Types for Proofs and Programs (TYPES'93), 1994: 127～165

[2] D'Argenio P R, Jeannet B, Jensen H E, et al.Reachability Analysis of Probabilistic Systems by Successive Refinements[J]. In Proceedings PAPM-PROBMIV'01, 2001: 39～56

[3] CCITT Fascicle VIII.3. CCCITT Recommendation X.25:Interface betweenDTEandDCEfor Terminals Operating in the Packet Mode on Public Data Networks[S], 1998.

[4] Groote J F, Pol J V D.A Bounded Retransmission Protocol for Large Data Packets[A]. AMAST'96[C]. 1996: 536～550

[5] D'Argenio P R, Katoen J P, Ruys T, et al.Modeling and Verifying a Bounded Retransmission Protocol[A]. In Proceedings of the COST 247 International Workshop on Applied Formal Methods in System Design[C]. 1996: 114～127

[6] Kwiatkowska M, Norman G, Parker D.www.cs.bham.ac.uk/～dxp/prism[EB/OL]

Modeling and Analysis of Bounded Retransmission Protocol in the Ad Hoc Network

CHEN Li-bin1, WEN Ying2
1. College of Computer Science, Hunan Institute of science and technology, Yueyang 414006, China 2. China Mobile Communication, Guangxi Nanning Corporation, Nanning 530028, China)

TP393

A

1672-5298(2010)01-0039-06

2010-12-12

陈立斌(1974- ), 男, 湖南武冈人, 湖南理工学院计算机学院讲师. 主要研究方向: 网络技术