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

【參考文獻(xiàn)】

相關(guān)期刊論文 前4條

1 黃廷輝;陸向遠(yuǎn);崔更申;楊e，

本文編號(hào)：2284374