Verification Of Routing Protocols Based On UPPAAL

The research results are emerging with the studies on Next Generation Internetant Internet of Things in recent years, and new communication and transmissionmethods are also emeraging. Many new routing protocols are essential part in thosenew-style networks. However, when designing a new routing protocol, bugs that canhardly be found manually will be introduced to the protocols inevitably due to theinherent complexity of routing protocols.Model checking is a formal verification technique that perform automaticverification on finite state systems. It provides the executive path which leads tosystem failures if the failures are exist. The reliability of routing protocols will beenhanced by applying model checking to find the flaws in protocol design. Timedautomata based model checking tool UPPAAL is a efficient tool to performreachability analysis, and been used frequently on verifying all kinds of real-timesystems includes network protocols. However, there are still two problems in theway of verifying routing protocols. Firstly, the diffculty of modeling them, as thecomplex timed data are diffcult to modeling. And secondly, the severe stateexplosion problem.Firstly, complex timed data that lie in routing protocols are studies in-depth. Adiscretization and abstraction based modeling method is proposed to solve thisproblem. The validity of this method is testified by experiment, and the performanceof this method is also analysized.Abstract technique and composition technique are introduced in the process ofmodeling to relief the state explosion. The model are decomposed to two submodelswhich are easier to be verified. The submodel are verified respectively, and theresults are composed to obtain the properties of the original model by the strategy ofassumption/assurance.Based on the abstract and compositional techniques and the modeling methodon complex timed data, a verification on OLSR routing protocol has carried out at the end of this paper. The experiment results show that OLSR protocol isdeadlock-free，consistent on protocol behavior and connected for all nodes. Theexperiment also shows that there exists redundant computaion in the routing tablecalculation part in OLSR protocol, and this redundancy can be reduced by delayingthe calculation.