An incidence matrix-based verification method for business process model in inter-domain network management system

Petri net has become one of the major formal methods for modeling and analyzing business processes. Petri net is utilized for business process modeling in inter-domain network management system. However business process models may contain errors. So model verification is of necessity and importance. A new model verification method is proposed based on incidence matrix of Petri net. It can be used to assess the correctness of business process models. The application of resource reservation in the inter-domain network management system is taken as an example to demonstrate the availability of the method.