Verification of Protocol BGP via Decomposition of Petri Net Model into Functional Subnets
Dmitry A. Zaitsev · 2005
Petri net model of the widely known protocol BGP of Internet backbone routing was constructed. The decomposition of Petri net model of communication protocol BGP into functional subnets was implemented. Invariance of the source model was proved on the base of established invariance of its functional subnets. The speed-up of computations obtained is exponential with respect to dimension of Petri net.