【摘要】：車載無線自組織網絡(VANET)是建立在移動車輛上的分布式移動通信和計算機網絡相結合的自組織通信網絡,有助于實現智能化的導航服務,降低交通事故發(fā)生的概率。高可靠路由協議是車載無線自組織網絡的關鍵技術,要求在無基礎設施支持下實現可信和穩(wěn)定的多跳信息傳輸,以保證智能交通系統(tǒng)中車輛安全。概率模型檢驗能夠遍歷系統(tǒng)全局狀態(tài)空間,緩解系統(tǒng)驗證中的狀態(tài)空間爆炸問題,有希望為VANET的高可靠路由協議分析與設計提供重要的手段。本學位論文首先深入研究城市車載節(jié)點移動特點,提出基于曼哈頓移動模型的改進模型,為車載無線自組織網絡(VANET)路由協議的研究打下基礎;接著利用概率模型檢驗技術研究VANET的AODV路由協議,并對該協議進行了優(yōu)化;最后研究VANET的GPSR路由協議,建立該協議的概率時間自動機模型并對比分析。本文的工作創(chuàng)新主要體現在以下三個方面:(1)提出一種基于改進曼哈頓移動模型的VANET城市車載移動模型,利用概率模型檢測技術將其建成離散時間馬爾科夫鏈模型(CTMCs),并使用概率模型檢測工具PRISM分析其節(jié)點移動狀態(tài)特征。(2)將概率模型檢測方法應用于VANET的AODV協議中,建立AODV協議的概率時間自動機模型,設計車載自組織無線網絡路由協議的可靠性、概率可達性、期望可達性等模型檢測中的評價公式,使用模型檢測工具PRISM對協議進行驗證,提出AODV協議路由維護過程的優(yōu)化方案。(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

【參考文獻】

相關期刊論文 前4條

1 黃廷輝;陸向遠;崔更申;楊e，

本文編號：2284374