Analyzing non-determinism in telecommunication services using P-invariant of Petri-net model

The non-deterministic behavior in telecommunication services are well-known as one of the most typical feature interactions, and they should be detected and eliminated from the telecommunication service specifications. The conventional analysis method of this non-determinism is based on reachability analysis. Since the method must exhaustively enumerate all reachable global states, it cannot be applied to the complex communication services which include many users. We propose an alternative method based on a Petri-net model. The method constructs a logically equivalent Petri-net for a given service specification, and obtains a set of states which cause the non-deterministic behavior using rules in the service specification. Then, the method identifies states in the set which are not reachable from the initial state using the P-invariant of the Petri-net, and deletes them from the set. As the P-invariant is utilized as the necessary condition, we must finally apply reachability analysis to states in the resultant set. Since the number of states in the resultant set may be reduced to a relatively small value the new method enables us to analyze the more complex services