Modeling and analyzing the convergence property of the BGP routing protocol in SPIN

The Border Gateway Protocol (BGP) is an interdomain routing protocol such that each autonomous system can independently formulate its routing policies. However, BGP does not always converge, because its routing policies may conflict and cause BGP to diverge, and result in persistent route oscillations. In this paper, we present an automated tool for verifying the convergence property of BGP by using the SPIN model checker. We have developed a SPIN library specifying a path vector protocol with a set of unspecified routing policies, and methods to instantiate the library to a specific BGP instance. The user only needs to provide models of network topology and customized routing policies, then SPIN can simulate the executions of the BGP instance, as well as automatically verify the protocol by exhaustively exploring all possible executions to detect possible divergences. The effectiveness of our library is demonstrated by experiments and verification results.