A Methodology For Verifying Routing Protocols Using Model Checking

The development of computer networks requires a large number of new routing protocols. Security and correctness of these routing protocols should be concerned. Currently, techniques and tools based on formal methods have been widely applied in analysis of routing protocols to help the design and implementation. However, on the one hand, routing protocols are diversified, and networks range from small-scale to large-scale. Hierarchical routing and artificial routing policies make routing algorithms which are clear concept and great performance to be complicated. Unreliable communication links and nodes lead to a dynamic network topology. On the other hand, formal methods are hard to understand. There are a lot of languages for specification and modelling and tools for formal verification. And these tools for formal methods are still very weak compared with what is theoretically possible. So, for network reasearchers it is hard and time consuming to select what languages, techniques and tools of formal verification are appropriate for routing protocol analysis.We proposed a valid methodology for verifying security and correctness of routing protocols. The methodology is based on model checking. Firstly, a model should be extracted by simplification and assumption about routing protocols. Secondly, the verification process and model refine is based on counter example guided avstraction refinement. Lastly, the methodology is applied in three routing protocols, and verifying security, correctness and convergence using model checker SPIN and CBMC. The result of verification shows that there methodology is valid and fesiable for verifying routing protocols.