A formal model for checking the convergence property of border gateway protocol

作者：Yin Ping^*; Ma Yinxue

来源：ICIC Express Letters, Part B: Applications , 2014, 5(6): 1753-1758.

• Autonomous systems
• Border gateway protocol
• Convergence problems
• Convergence properties
• Interdomain Routing
• Routing information
• SPIN
• Variable parameters

The Border Gateway Protocol (BGP) is an important inter-domain routing protocol in Internet. It allows independent policies on each Autonomous System (AS). However, the flexibility in designing policies causes the convergence problem, i.e., a BGP network constantly sends routing informations between ASes and cannot reach a stable state. In this paper, 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. Our model is intuitive and general enough, thus different instances of BGP networks can be simulated and verified by modifying some variable parameters and policies. Finally, we simulate and verify some selected BGP networks instances by using the SPIN model checker.

• 出版日期2014
• 单位南京航空航天大学; 江南大学