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

Probability model checking for random back off mechanism in vehicle network communication protocol

作　　者：金丽[1] 章国安[1] 朱浩[1] 段玮 朱晓军[1] JIN Li;ZHANG Guoan;ZHU Hao;DUAN Wei;ZHU Xiaojun(School of Information Science and Technology,Nantong University,Nantong 226019,China)

机构地区：[1]南通大学信息科学技术学院,江苏南通226019

出　　处：《南通大学学报（自然科学版）》2022年第2期38-48,共11页Journal of Nantong University(Natural Science Edition)　

基　　金：国家自然科学基金面上项目(61971245)。

摘　　要：针对车联网IEEE 802.11P通信协议应用于车与车之间的短程通信以提高数据传输效率,提出了该通信协议中随机退避机制的模型检测方法。分析了分布式协调功能的基本接入技术,从多个属性角度对双向握手机制中的随机退避过程进行了深入地分析与验证;建立了双向握手机制的车辆通信系统网络模型、基于概率时间自动机的共享信道模型及基于马尔可夫决策过程的随机退避状态转移过程;使用概率时间自动机语法、语义规则及其相关定理、推论建立了随机退避过程的数学模型;基于概率模型检测方法对相关模型进行验证和性能分析。仿真分析结果表明:所有的到达状态均满足概率连续随机计算数逻辑属性定义公式要求,车与车之间在短距离数据通信传输中具有较高的成功率,验证了IEEE 802.11P协议在车辆短程通信中具有良好的表现性,确保了车联网链路生存性,为车联网通信链路连通性分析提供了研究基础。Aiming at the applications of IEEE 802.11P communication protocol in vehicle networks for efficient short-range communications,a model checking of random backoff mechanism for IEEE 802.11P is proposed.The basic access technology for distributed coordination function(DCF)in IEEE 802.11P is emphatically analyzed.Specifically,the random backoff process in two-way handshake system is analyzed and verified;a network model of vehicle communication system based on bidirectional handshake mechanism is established,and the shared channel model based on probabilistic timed automata(PTA)is also provided.With this model,a PTA-based sharing channel model is proposed,a Markov decision process(MDP)-based random backoff state transfer process is considered according to the random back off mechanism,the mathematical abstract model of the random backoff process is established by using PTA syntax,semantic rules and their related theorems and inferences.Moreover,based on the time-varying probability model,arrival analysis of the proposed abstract model is conducted.The results show that all the arrival states meet the requirements of the probabilistic computational tree logic(PCTL)attribute definition formula.A high success rate between vehicles in short-range data communication transmission verifies the advantages of IEEE 802.11P protocol,which also ensures the survivability of vehicle networks.This model checking method also provides a research basis for communication link connectivity analysis in vehicle networks.

关 键 词：车联网 IEEE 802.11P 退避机制 模型检测 

分 类 号：TN915.04[电子电信—通信与信息系统]