Probabilistic verification of BGP convergence

The Border Gateway Protocol (BGP) is the de facto Internet routing protocol. Various aspects of the BGP protocol have been analyzed using mathematical and experimental approaches. Formal verification of BGP specification validates whether or not a specific set of requirements is satisfied. In resent years, the probabilistic behavior of BGP has been explored. The size of routing tables has been modeled as a stochastic process that changes over time according to some probability distribution function. Hence, the verification of BGP may also be probabilistic in nature due to its randomized behavior. In this paper, we present a probabilistic model checking approach to analyze BGP convergence properties that may be employed to automate the BGP convergence analysis.