基于概率模型检验的车载无线自组织网络路由协议研究
发布时间：2018-10-21 07:32
【摘要】：车载无线自组织网络(VANET)是建立在移动车辆上的分布式移动通信和计算机网络相结合的自组织通信网络,有助于实现智能化的导航服务,降低交通事故发生的概率。高可靠路由协议是车载无线自组织网络的关键技术,要求在无基础设施支持下实现可信和稳定的多跳信息传输,以保证智能交通系统中车辆安全。概率模型检验能够遍历系统全局状态空间,缓解系统验证中的状态空间爆炸问题,有希望为VANET的高可靠路由协议分析与设计提供重要的手段。本学位论文首先深入研究城市车载节点移动特点,提出基于曼哈顿移动模型的改进模型,为车载无线自组织网络(VANET)路由协议的研究打下基础;接着利用概率模型检验技术研究VANET的AODV路由协议,并对该协议进行了优化;最后研究VANET的GPSR路由协议,建立该协议的概率时间自动机模型并对比分析。本文的工作创新主要体现在以下三个方面:(1)提出一种基于改进曼哈顿移动模型的VANET城市车载移动模型,利用概率模型检测技术将其建成离散时间马尔科夫链模型(CTMCs),并使用概率模型检测工具PRISM分析其节点移动状态特征。(2)将概率模型检测方法应用于VANET的AODV协议中,建立AODV协议的概率时间自动机模型,设计车载自组织无线网络路由协议的可靠性、概率可达性、期望可达性等模型检测中的评价公式,使用模型检测工具PRISM对协议进行验证,提出AODV协议路由维护过程的优化方案。(3)建立VANET的GPSR路由协议概率时间自动机模型,设计GPSR协议的可靠性、概率可达性、期望可达性等模型检测中评价公式,使用模型检测工具PRISM对协议进行验证与分析。
[Abstract]:Vehicle-mounted wireless ad hoc network (VANET) is a self-organized communication network based on distributed mobile communication and computer network. It is helpful to realize intelligent navigation service and reduce the probability of traffic accidents. High reliability routing protocol is the key technology of vehicular wireless ad hoc networks. It requires reliable and stable multi-hop information transmission without the support of infrastructure to ensure the security of vehicles in intelligent transportation systems. Probabilistic model checking can traverse the global state space of the system, alleviate the explosion of the state space in the system verification, and hopefully provide an important means for the analysis and design of the high reliability routing protocol of VANET. In this thesis, firstly, the characteristics of urban vehicular node mobility are deeply studied, and an improved model based on Manhattan mobile model is proposed, which lays a foundation for the research of (VANET) routing protocol in vehicular wireless ad hoc networks. Then the AODV routing protocol of VANET is studied by using probabilistic model checking technique, and the protocol is optimized. Finally, the GPSR routing protocol of VANET is studied, and the probabilistic time automaton model of the protocol is established and compared. The work innovation of this paper is mainly reflected in the following three aspects: (1) A VANET urban vehicular mobile model based on the improved Manhattan mobile model is proposed. The probabilistic model detection technique is used to build the discrete time Markov chain model (CTMCs),) and the probabilistic model checking tool (PRISM) is used to analyze the mobile state of the nodes. (2) the probabilistic model detection method is applied to the AODV protocol of VANET. The probabilistic time automata model of AODV protocol is established, and the evaluation formulas of the routing protocol in vehicle Ad Hoc wireless network are designed, such as reliability, probability reachability and expected reachability. The protocol is verified by model checking tool PRISM. The optimization scheme of AODV protocol routing maintenance process is proposed. (3) the GPSR routing protocol probabilistic timed automata model of VANET is established, and the evaluation formulas of GPSR protocol reliability, probabilistic reachability and expected reachability are designed. Model checking tool PRISM is used to verify and analyze the protocol.
【学位授予单位】：南京邮电大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：U495;TN929.5
[Abstract]:Vehicle-mounted wireless ad hoc network (VANET) is a self-organized communication network based on distributed mobile communication and computer network. It is helpful to realize intelligent navigation service and reduce the probability of traffic accidents. High reliability routing protocol is the key technology of vehicular wireless ad hoc networks. It requires reliable and stable multi-hop information transmission without the support of infrastructure to ensure the security of vehicles in intelligent transportation systems. Probabilistic model checking can traverse the global state space of the system, alleviate the explosion of the state space in the system verification, and hopefully provide an important means for the analysis and design of the high reliability routing protocol of VANET. In this thesis, firstly, the characteristics of urban vehicular node mobility are deeply studied, and an improved model based on Manhattan mobile model is proposed, which lays a foundation for the research of (VANET) routing protocol in vehicular wireless ad hoc networks. Then the AODV routing protocol of VANET is studied by using probabilistic model checking technique, and the protocol is optimized. Finally, the GPSR routing protocol of VANET is studied, and the probabilistic time automaton model of the protocol is established and compared. The work innovation of this paper is mainly reflected in the following three aspects: (1) A VANET urban vehicular mobile model based on the improved Manhattan mobile model is proposed. The probabilistic model detection technique is used to build the discrete time Markov chain model (CTMCs),) and the probabilistic model checking tool (PRISM) is used to analyze the mobile state of the nodes. (2) the probabilistic model detection method is applied to the AODV protocol of VANET. The probabilistic time automata model of AODV protocol is established, and the evaluation formulas of the routing protocol in vehicle Ad Hoc wireless network are designed, such as reliability, probability reachability and expected reachability. The protocol is verified by model checking tool PRISM. The optimization scheme of AODV protocol routing maintenance process is proposed. (3) the GPSR routing protocol probabilistic timed automata model of VANET is established, and the evaluation formulas of GPSR protocol reliability, probabilistic reachability and expected reachability are designed. Model checking tool PRISM is used to verify and analyze the protocol.
【学位授予单位】：南京邮电大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：U495;TN929.5
【参考文献】
相关期刊论文 前4条
1 黄廷辉;陆向远;崔更申;杨e，
本文编号：2284374
本文链接：https://www.wllwen.com/kejilunwen/xinxigongchenglunwen/2284374.html
