In: Zviazok (Communications), no. 1(53), pages 41-47. 2005. In Russian.
Abstract: The technique for verification of telecommunication protocols with the aid of decomposition of Petri net models is presented. Detailed Petri net models of telecommunication protocols contain hundreds and sometimes thousands of nodes. Such a dimension makes their analysis by the formal methods based on application of fundamental equation and linear invariants practically unfeasible. Decomposition of Petri net model into functional subnets allows the obtaining the exponential speed-up of computations. Presented technique was studied in details on the example of verification for wide-known protocol BGP of Internet backbone routing.
Keywords: telecommunication protocol; verification; Petri net; invariant; decomposition; functional subnet.