Research On Routing Protocol Of Vehicle Wireless Self-organizing Network Based On Probability Model Checking

The VANET is a kind of communication network which is based on distributed mobile communication network and computer network which can provide intelligent navigation service and reduce the probability of traffic accidents.The high reliable routing protocol is one of the key technology in the VANET,which requires to realize reliable and stable multi hop information transmission without any infrastructure support.So it can make sure the safety of vehicles in intelligent transportation system.The probabilistic model checking technology can traverse the global state space of the system and alleviate the problem of state space explosion.It is expected to provide an important means for the analysis and design of high reliable routing protocols in vehicular ad hoc networks.In order to research of the VANET routing protocol,this thesis firstly studies the characteristics of urban vehicle node movement,and proposes an improved model based on Manhattan mobile model.Then an optimization scheme of the AODV protocol is proposed.Finally,the probability time automaton model of GPSR protocol is established and compared with the improved AODV protocol.The major works of this thesis are as follows:Firstly,this thesis proposes an improved vehicle movement model based on Manhattan mobile model.And then we construct the discrete-time Markov chain model(CTMCs)for the improved vehicle movement model.Then we analaze the characteristics of node mobility and the influence on vehicle wireless communication based on the probabilistic model detection tool – PRISM.Secondly,this thesis establishes the Probabilistic Time Automata Models of the AODV routing protocols based on probabilistic model detection method.Then many formulas in Probability model detection such as reliability formulas,probability reachability formulas and pxpected accessibility formulas are designed for the VANET Routing Protocol.An optimization scheme of theAODV protocol is proposedFinally,this thesis studies the GPSR protocol and establishes the model and designed formulas by using the same technology.the model detection tool PRISM is used to verify the protocol and compared with the AODV protocol.