车联网通信协议中随机退避机制的概率模型检测

金 丽，章国安，朱 浩，段 玮，朱晓军

（南通大学 信息科学技术学院，江苏 南通 226019）

道路交通安全问题是车联网研究的重要内容，专用短程通信IEEE 802.11P 协议是智能交通系统的重要组成部分[1-5]，它能保证车联网中车与车之间短距离通信，大量减少道路上的碰撞事故。IEEE 802.11P 是基于国际标准IEEE 802.11 设计的，设计中明确以最严格的性能指标满足V2X[6-8]应用的所有需求。1999 年，美国联邦通信委员会为V2X在5.9 GHz 区域中留出75 MHz 的带宽，并把此作为IEEE 802.11P 标准的工作频段，该标准于2009 年获得批准。IEEE 802.11p 技术中采用了载波侦听多路访问/避免碰撞（carrier sense multiple access with collision avoidance，CSMA/CA）机制[9-10]，该机制采用随机指数退避规则最小化数据包传输碰撞值。

有关IEEE 802.11P 通信协议研究中，Rezgui等[11]人基于分布式协调功能（distibuted coordination function，DCF）机制提出了车辆单位时间内成功接收信息的吞吐量、车辆成功接收信息的概率，以及平均延迟时间的数学推导结果和模拟数值仿真分析。Almohammedi 等[12]人通过数学推导数据包成功发送的延迟时间、计算服务程序中的饱和吞吐量、数据包成功发送的平均数量等公式进行数值模拟仿真分析研究IEEE802.11p/1609.4 在车联网中的性能。Yao 等[13]人基于IEEE802.11p/1609.4 标准建立了计算带宽资源分配的数学分析模型，并对模型进行了数值近似模拟仿真。Gopinath 等[14]人在研究IEEE802.11P/1609.4 标准协议中提出采用NS3 和SUMO 两个仿真工具模拟仿真车辆数据传输情况。文献[15-20]通过数学推导对该协议机制性能进行模拟仿真或数值分析。本文将使用概率模型检测[21-22]来自动验证IEEE 802.11P 介质访问控制子协议，并对该协议机制建立一个随机过程，如马尔可夫决策过程（Markov decision process，MDP）[23]，概率模型检测算法检测模型中每个状态是否满足具体的概率属性。在模型建立中，选择使用IEEE 802.11P 介质访问控制方案的双向握手机制，它是由两个发送站和两个目的站组成的网络结构。建模形式为概率时间自动机（probabilistic timed automata，PTA)[24]，概率时间自动机是时间自动机（timed automata，TA）的扩展[25]，它的离散概率分布在控制图的边缘。为了减少概率模型检测中的复杂度，本文首先采用TA 验证了PTA 中的几个抽象模型，由此产生了较小的PTA，采用离散时间语义属性得出有限状态的马尔可夫决策过程；然后使用概率模型检测工具（probabilistic symbolic model checker，PRISM）[26]来验证重复传输碰撞的可能性和车辆发送点在一定时间单元内正确发送数据包的概率；最后通过定义相关到达概率属性，进行概率模型检测。数值分析结果表明：车载自组织网络基于IEEE 802.11P 通信协议在短距离数据通信传输中具有较高的传输成功率，在车辆与车辆之间通信中具有良好的链路连通性，保证了车载自组织网络在一定时间和距离内具有可生存性；另外，所采用的概率模型检测器方法与手工运算推导公式再进行模拟仿真的方法相比，它不仅运算效率高、节省时间，还可以针对各个并行异步模块组成的非确定性系统建模，从多个属性角度进行模型分析和数值仿真。

1 接入技术

1.1 分布式协调功能接入机制

分布式协调功能（distibuted coordination function，DCF）是IEEE 802.11P 通信协议的信道接入机制[27-28]，其基于CSMA/CA 协议，它的一个重要特征是具有随机的、时隙的指数退避特征，它旨在打破重复先前失败传输站点之间的均衡性。

由于IEEE 802.11P 指定发送站点在传输之前侦听信道，如果多个站点同时处于易损期，则可能发生冲突。例如，如果发送站点1 处于易损期，当它开始发送数据时，那么其他发送站点在某种延迟之后（等于易损时期的长度）才能检测到站点1 的传输，然而这阶段另一个发送站点也可能开始传输数据，这样就会导致碰撞。

DCF 有两种传输机制，分别为基本接入机制和RTS/CTS 四次握手接入机制，它们的区别在于后者在数据传输之前有RTS 询问和CTS 应答。本文重点研究基本接入机制，该机制基本工作原理是：当无线局域网络中一个站点准备发送一个新的数据包时，它首先侦听信道是否在一个DCF 帧间间隔（distibuted coordination function interfame space，DIFS）内空闲，DIFS 的长度取决于物理层并且至少和易损期的长度相等；如果在此期间该信道是空闲的，那么该站点可以向目的站点传输数据包；在传输终止时，发送站点立即侦听信道，以检测是否有另一个站点当前正在传输，如果有，那么两站点数据包将发生碰撞，否则该发送站点等待目的站点发送一个确认（Ack）信息。因为发送站点不能监听自身的传输，所以目的站点必须发送确认信息，表示数据包传输成功。为了减少发送过程中碰撞导致数据包传输失败，DCF 将随机退避机制和CSMA/CA 接入方式相结合，当发送站发生以下情况之一时，发送站将进入退避过程：1）发送站点在一个DIFS 期间内没有侦听到信道空闲；2）在发送站点完成一个数据包传送后信道仍处于忙状态；3）发送站点在超时前未接收到目的站点的成功传输确认信息；4）发送站点收到确认信息又准备发送下一个数据包。

1.2 随机退避机制

随机退避机制是一种能降低数据包传输过程中发生碰撞的有效方法，它包含退避过程中随机退避值的选择。在随机退避过程中，首先，发送站点需侦听信道，如果信道忙，那么等待到它处于空闲时再发送，这时还需继续进行侦听直到信道空闲为一个DIFS。接着，随机选择退避值，它表示为“时隙”的时间段的数目。这些时间段必须通过才能开始传输，其中时隙的持续时间是由A slot time 给出的，并且必须至少与易损期一样长。如果检测到信道空闲为一个A slot time，则退避值将减1 递减；如果此时检测到信道有数据包传输，则退避值递减暂停，直到信道被检测到空闲为一个DIFS，退避值继续从原来暂停值处开始递减直到为0。最后，重新恢复开始传输状态。

如图1 是一个退避过程应用，假设车联网中有4 辆车，分别为车辆1、车辆2、车辆3 和车辆4。车辆1 准备向目的车辆3 发送数据包，而车辆2 刚完成向目的车辆4 发送数据包，在车辆2 完成传输得到车辆4 的确认信息后，等待一个DIFS 时间继而随机选择退避值9，然后车辆2 每经过一个A slot time，它的退避值则减1，然而在车辆2 的退避值未减到0 之前车辆1 侦听到信道在一个DIFS 时间内是空闲的，它便开始向车辆3 发送数据包，这时信道处于忙状态，车辆2 的当前退避值立即暂停减1并保存，等待车辆1 完成数据包传输，经过一个短帧间隔（short interfame space，SIFS）时间，得到目的车辆3 的确认信息，再经过一个DIFS 时间后车辆2的退避值在原来暂停保存值上继续进行减1 直到0。在车辆2 的退避值进行暂停到继续减1 这一过程称为冻结退避值时间，这个时间段信道属于占用（忙）状态。在整个退避过程中，802.11P 中规定SIFS 时间单位小于DIFS 时间单位，在退避值结束前发送站必须要先检测信道在一个DIFS 时间单位内是否空闲。

图1 车联网中两车节点间的退避过程Fig.1 Back off procedure between two vehicles in vehicle networks

在上述退避过程中，随机退避值的选择在整数范围[0，CW]（争用窗口）内上均匀分布，窗口值计算公式为CW=（aCWmin+1）× 2bc-1，其中aCWmin是物理层给出的常数，bc 为变量，表示退避计数器，初值设为0，说明了那些挂起的数据包未成功重传的数量。退避计数器可以设置一个上限，用bcmax表示，通过另一个物理层常数计算得到。

2 模型建立

2.1 通信模型建立

本文重点是研究IEEE 802.11P 的DCF 接入机制中的基本接入机制。在车联网系统中选用任意4辆临近车节点，它们相互之间可能存在信息传输，其对应车辆通信模型如图2 所示，包括3 个模块，其中车节点1 和车节点2 为发送模块，车节点3 和车节点4 为目标接收模块，以及双方进行信息传输的信道模块。图中车节点1 和车节点2 共享同一信道分别与车节点3 和车节点4 进行数据通信。由于信道资源共享，容易引起发送车辆节点数据包碰撞问题而导致双方通信失败。为了研究发送车节点数据传输过程产生碰撞问题，基于PTA 理论设计了两个发送车节点的通信信道模型如图3 所示，图中两个车节点进行数据发送，其中行为状态Si包含3 种情况：当Si=0 时，表示信道中无数据传输；当Si=1 时，表示信道中有数据传输；当Si=2 时，表示信道中数据传输混乱（即有数据碰撞发生）。在信道PTA 模型中，i 取值为1 或2，两个变量S1和S2分别表示车节点1 和车节点2 发送数据包的状态，其中车节点1 发送时，用S1:=min（S2+1，2）表示当前的状态，用S2:=min（S2+S2，2）表示车节点2 的状态；当车节点2 发送时，同样采用类似形式表达状态。信道作为公共资源，既承担发送车节点的数据包传送任务，也承担着目标车节点收到数据包向发送节点返回确认信息的传送任务。

图2 车辆通信模型Fig.2 Model of the vehicle communication

图3 车辆信道PTA 模型Fig.3 PTA model of the vehicle channel

2.2 随机退避机制的马尔可夫决策过程模型建立

车节点在信道传输数据过程中遵循IEEE 802.11P 的退避机制，由于退避过程具有随机不确定概率行为，可通过建立MDP 来解决非确定性概率行为。根据MDP 的定义，建立了发送车节点的退避机制状态转换图，如图4 所示，车节点1 检测信道空闲（载波侦听信道），等待一个DIFS 后，预约信道，如果此期间内超过信道易损期（可能存在发送节点2 正传输数据包），表明信道预约成功，车节点1 开始发送数据包，此时状态设为S1。当数据包完成传输时间不低于传送的最小设置时间Tmin和不超过传送的最大设置时间Tmax时，表明数据包发送完成。这时还需再次检测信道在一个SIFS 内是否空闲，如果空闲，即S1+S2=0，那么目标车节点3 给车节点1 发送一个确认（Ack）信号。车节点1 如果在一个确认时间Ack_time 内收到Ack，则表明发送任务成功；否则表明超时，继续等待信道空闲，等待DIFS，进入退避过程，退避计数器进行减1 计数，判断是否过易损期，再次重复之前信道预约传输数据包过程。例如，当一个车节点发送完数据包准备再次发送时，它必须先等到信道空闲一个DIFS，如果信道仍忙，则进入退避过程，退避计数器进行随机退避计数backoff :=RAND{bc}（其中bc 为退避计数器的值，它的值不超过退避最大值（bomax=6），退避值在每个时隙时间长度A slot time 上进行减1，直到退避计数为0，且易损期过后才可再次进行数据包发送任务，具体参数设置和描述如表1 所示。

图4 发送车节点MDP 状态转换图Fig.4 MDP status transition diagram of the sending vehicle

表1 参数设置和具体描述Tab.1 Notation of the model parameters

2.3 概率时间自动机模型建立

根据PTA 的语法和语义规则[29]，将对通信模型建立抽象数学模型，假设车载网络用PTAVN表示，两个发送车节点概率时间自动机模型分别用PTAVS1、PTAVS2表示，信道模型用PTACh表示，目标车节点概率自动机分别用PTAVD1和PTAVD2表示。由于目标车节点行为是确定的，所以把它们组合到发送车节点的概率自动机中，分别用PTAVS1′和PTAVS2′表示，其中PTAVS1′=PTAVS1‖PTAVD1，PTAVS2′=PTAVS2‖PTAVD2。另外，数据包发送和确认信息都使用同一个信道进行传输，信道的自动机可以细化为PTACh′表示，那么可以得到系统抽象模型为

在抽象模型中，对于PTA 之前的概率模型，用FPTA（formerly probabilistic timed automaton）来 表示，假设PTAVN之前的概率模型用FPTAVN来表示，对于发送车节点的PTA 之前的PTA，分别用FPTAVS1和FPTAVS2表示，PTACh之前信道PTA 用FPTACh表示，PTAVD1和PTAVD2分别用FPTAVD1和FPTAVD2表示；同样对于PTAVN′而言，它之前的概率模型用FPTAVN表示，PTAVS1′和PTAVS2′之前的概率模型分别用FPTAVS1′和FPTAVS2′表示，PTACh′之前的概率模型用FPTACh′表示，那么得到之前的抽象模型为

经过模型检测器和转移系统迹分布验证，可以得到

由式（1）—式（5）得出结论

在IEEE 802.11P 的DCF 基本接入机制中，由于没有紧急行为操作，一切的行为操作都是按照预先设定的随机退避机制进行，所以之前网络的PTA表示为LPTA 或LTA。根据PTA 理论[30-31]可得根据得到的结论，通过概率模型检测器对该抽象系统模型在时间变化上进行概率分析，具体通过定义相关属性，讨论系统模型在不同时间内最小和最大到达性分析。

3 系统模型概率检测

3.1 模型验证

在模型验证过程中，根据不同的最大退避值bomax和不同的数据包传输时间Tmax条件，对系统状态数、模型建立情况及到达计算进行统计和分析。模型分析基于Intel 内核、3.4 GHz 处理器、64 位Windows7 版本的操作系统、在PRISM 4.4 模型检测器中进行。当Tmax=500 μs 时，模型检测情况如表2所示，随着bomax的增大，模型状态数和多终端二元决策图中的节点数也随之增多，模型建立时间也随之变大，迭代数和迭代时间也随之增大。

表2 Tmax=500 μs 下的模型运行情况Tab.2 PRISM model checking results with Tmax=500 μs

为了比较在不同bomax下模型检测验证情况，考虑增加数据包传输时间Tmax的设定值，当Tmax=1 000 μs 和Tmax=2 000 μs 时，模型运行情况分别如表3 和4 所示。

从表3 和4 中可以得出，随着设定数据包传输时间的变大，对于相同的bomax，模型状态数、多终端二元决策图中的节点数、模型建立时间和迭代数，它们之间的增量随着Tmax设定值的变化而不变，多终端二元决策图中的终端节点数随着Tmax设定值的变化也保持不变。另外，表1、2 和3 得出同样的结果，即模型状态数随着bomax的增大而增多。

表3 Tmax=1 000 μs 下的模型运行情况Tab.3 PRISM model checking results with Tmax=1 000 μs

表4 Tmax=2 000 μs 下的模型运行情况Tab.4 PRISM model checking results with Tmax=2 000 μs

3.2 系统模型状态到达概率分析

3.2.1 概率到达性分析

概率到达性分析是PRISM 的核心运算部分，将产生节点数、终端节点数和计算到达性的迭代数和迭代时间。在定义概率到达性属性前，PRISM 模型检测器对发送车节点的发送过程状态进行了描述，具体如表5 所示，一共有12 个状态，其中状态11 将在PCTL 概率度量属性定义运用。

表5 车节点发送状态情况描述Tab.5 Description of the sending vehicle status

具体概率属性定义公式和模型检测结果如下：

1）属性定义1 P≥1[ture∪v1=11&v2=11]。式中“≥”是关系操作，表示下界，与P 的最小概率相对应。该式指在最小概率为1 的情形下两个发送车节点都成功发送数据包，模型检测时间如表6 所示，随着bomax的增大，模型检测时间、迭代数及迭代时间都增大。

表6 概率到达性模型检测时间Tab.6 Model checking time of probabilistic reachability

模型验证结果如图5 所示，结果表明车节点在初始状态下满足属性要求。

图5 概率到达性模型验证结果Fig.5 Model result of the probabilistic reachability

2）属性定义2 Pmax=?[ture∪col=k]。该属性公式表示发送车节点碰撞次数到达k 的最大概率。表7 中列举了到达碰撞次数分别为2、3、4、5、6 情况下的概率，表中情况说明随着到达碰撞次数越大，发生的概率越小；当碰撞次数大于4 时，随着退避值的增大，发生的概率一样。

表7 发送车节点碰撞次数到达k 的最大概率Tab.7 Maximum probability of k collisions in the sending vehicle

3.2.2 基于时间边界的概率到达性分析

在上述概率分析基础上，本节对模型进行时间边界的约束，分析了两个发送车节点在规定时间T内成功传输数据包的最小概率情况（最大概率为1），具体属性公式定义如下：

1）属性定义3 Pmin1=?[ture∪v1=11&v2=11&t≤T]。该属性公式表示在规定时间T 内，两个发送车节点都能成功完成数据包传输的最小概率。

2）属性定义4 Pmin2=?[ture∪（v1=11v2=11）&t≤T]。该属性公式表示在规定时间T 内，两个发送车节点中任意一个车节点成功完成数据包传输的最小概率。

3）属性定义5 Pmin3=?[ture∪v1=11&t≤T]。该属性公式表示在规定时间T 内，发送车节点1 成功完成数据包传输的最小概率。

根据以上3 个属性公式定义，分析了它们在不同T 时间内的模型检测概率情况如图6、7 所示，在图6 中，数据包发送成功的概率随时间变化不同，其中任意一个车节点的数据包成功传送率高于两者同时传送的成功率；在图7 中，在发送数据包完成时间少的情况下，随着时间的增长，车节点间的数据包成功传送率越大，则网络生存性越高；发送数据包的时间越长，车节点间的数据包成功传送率越小，那么网络生存性越低。研究结果表明802.11P协议中的退避算法符合车联网节点通信环境需求，在短距离传输信息上具有很好的表现性。

图6 T≤100 内3 种属性的最小概率比较Fig.6 Minimum probability comparison of three attributes within T≤100

图7 T≤100 内在不同的传输数据包最大时间下最小概率比较Fig.7 Minimum probability comparison of different transmission packets within T≤100

3.2.3 期望到达性分析

使用Reward 结构用于期望值分析。到达性的期望属性定义如下：

1）属性定义6 Rmax{"col"}=?[Fv1=11&v2=11]。该属性公式表示在两个发送车节点成功发送数据包之前的最大期望碰撞次数，模型检测的结果如表8 所示。在两个发送车节点成功发送数据包之前，随着退避值由0～6 变化，到达性的迭代数和迭代时间都随之增加，但是最大碰撞期望值近似相等，约为1.2 次，不超过两次，信道传输性能良好。

表8 期望最大碰撞数的模型检测结果Tab.8 Model checking result of expected maximum collision numbers

2）属性定义7 R1max{"cos t"}=?[Fv1=11&v2=11]。该属性公式表示在两个发送车节点都成功发送数据包之前的最大期望丢包数。模型检测的结果如图8 所示，当最大退避值为0 时的期望丢包数最小；当最大退避值为1～6 时，随着数据包最大传输时间的增大，期望丢包数比最大退避值为0 时的丢包数大幅度增长，但是随着最大退避值大于1，所有的期望丢包数都近似相等。

3）属性定义8 R2max{"cos t"}=?[Fv1=1111]。该属性公式表示在两个发送车节点中其中一个车节点成功发送数据包之前的最大期望丢包数。模型检测结果如图9 所示，图中最大期望丢包数量随时间变化情况和图8 情况类似。为了进一步比较它们两者的丢包情况，因为两者在最大退避值大于1时最大期望丢包数近似相等，所以模型检测分析针对两种情况下最大退避值分别为0 和1 的情形进行了比较。具体比较情况如图10 所示，图中当最大退避值为0 时，两车节点中任一车节点成功传输数据包之前的最大期望丢包数量低于两车节点都成功传输数据包之前的最大期望丢包数量；当最大退避值大于0 时，两者最大期望丢包数量在最大传输时间为300 μs 以内时近似相等；但是当最大传输时间大于300 μs 时，两车节点中任一车节点成功传输数据包之前的最大期望丢包数量略低于两车节点都成功传输数据包之前的最大期望丢包数量，模型检测结果表明满足属性公式定义。

图8 最大期望丢包数随时间的变化曲线（v1＆ v2）Fig.8 Maximum expected number of lost packets with maximum transmission time（v1＆ v2）

图9 最大期望丢包数随时间的变化曲线（v1│v2）Fig.9 Maximum expected number of lost packets with maximum transmission time（v1│v2）

图10 两种发送情况下最大期望丢包数随时间的变化比较Fig.10 Comparison of maximum expected lost packets in two sending vehicles with maximum transmission time

4 结论

本文分析了车联网短程通信IEEE 802.11P 协议，研究了分布式协调功能DCF 的基本接入技术，并详细分析了该技术中的双向握手机制，使用数轴图的形式对其中的随机退避过程进行了具体剖析；提出了基于双向握手机制的车辆通信系统网络模型，根据该通信网络模型的发送车辆节点和目标车辆节点的数据包传输情况，以及信道的使用情况建立了基于概率时间自动机PTA 的共享信道模型，建立了基于MDP 的随机退避过程，并使用概率时间自动机相关理论对随机退避过程建立数学模型；提出了使用概率模型检测方法对该数学模型进行检测和验证，通过定义相关满足约束条件的属性公式对模型中各个状态随时间变化的到达概率情况、期望值情况进行数值分析。分析验证结果表明，车载网络在IEEE 802.11P 通信协议下其短距离数据通信传输中具有较高的传输成功率，在车辆与车辆之间通信中具有良好的链路连通性，保证了车载网络在一定时间和距离内具有可生存性。另外所提出的概率模型检测器方法不同于传统的手工推导数学分析和仿真方法，它能进行自动状态检测，在定义各种属性条件下，它能自动完成所有的状态搜索、迭代计算、到达性分析、基于时间边界的各种度量分析，以及期望值分析，这为分析车联网通信链路连通性提供了借鉴。