Verification of Protocol ECMA with Decomposition of Petri Net Model

摘要

Decomposition of Petri net model of ECMA communication protocol into minimal functional subnets, left and right communicating systems, subsystems of connection establishing and disconnecting is implemented. A correct protocol ought to be invariant one. Invariance of source model is proved on the base of established invariance of functional subnets. Isomorphism of subnets has allowed the calculation of invariants in the process of consecutive composition of net. Acceleration of computations for decomposition technique was estimated. It is exponential with the respect to net dimension.