Until now, in a communication system which deals with multiple processes, system behavior has been described by a fixed number of processes. The state reachability problem for specified processes was generally deliberated within a pre-defined number of processes, and was analyzed by essentially searching for all possible behaviors. However, in a system whose number of processes is arbitrary, a given state which is not reachable in some situations which consists of a small number of processes might be reachable in another situation which consists of a larger number of processes. This article discusses the above problem, assuming that the behavior of a system is described by an arbitrary number of processes. After discussing the relationship between our model and the Petri net model, we clarify the properties between the set of reachable states and the number of processes involved in the system, and show an algorithm to obtain a sufficient number of processes for resolving the reachability problem.

This paper gives a verification method of a service specification in a communication system by utilizing Petri net. We define a service specification and clarify the feature of the specification. And we discuss a relation between a service specification and Petri net which represents the specification. Furthermore, this paper describes some kinds of verification for the specification and shows several examples. We are now developing a software support system-EXPRESS (EXPeRt system for ESS). EXPRESS designs automatically the service specification from user's requirements. In EXPRESS, each requirement is converted into ISG (Individual Service Graph) and all ISGs are integrated into TSG (Total Service Graph). TSG is the final service specification. ISG and TSG are described by using Petri net. Petri net is used for modeling a communication protocol and an asynchronous system. A service starts from an idle state and returns to the same idle state in a communication system. This means that a service specification should have a t-invariant. And a t-invariant which can not be decomposed is called a prime service. The followings are needed for verification of the specification: verification of ISG, detection of ISG from TSG and detection of other prime services than ISG. These are verified by utilizing an analysis of Petri net.