doi: 10.4304/jsw.9.6.1619-1625
Model checking the convergence property of BGP networks
- 1 School of Science, Jiangnan University, Wuxi 214122, China
- 2 College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China
Abstract
The Border Gateway Protocol (BGP) is an important inter-domain routing protocol, which is widely used in Internet. It allows independent policies to be designed for each Autonomous System (AS). However, the flexibility in designing independent policies causes the convergence problem, i.e., a BGP network may constantly send routing information between ASes and cannot reach a stable state. In this paper, we propose an approach for model checking the convergence property of BGP networks. We firstly establish a formal model of BGP networks and define its convergence property. Then we use the Promela language to describe this model and analyze its convergence. The model is generic enough, thus different instances of BGP networks can be simulated and verified by only modifying parameters and policies. Finally, as examples, we simulate and verify some typical instances of BGP networks by using the SPIN model checker.
Keywords
- border gateway protocol
- BGP
- model chec
How to Cite
Ping Yin, Yinxue Ma, and Zhe Chen, "Model checking the convergence property of BGP networks," Journal of Software, vol. 9, no. 6, pp. 1619-1625, 2014. https://doi.org/ 10.4304/jsw.9.6.1619-1625
Copyright & License
Copyright © 2014 by the authors. This is an open access article distributed under the Creative Commons Attribution License which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited (CC BY 4.0).