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.

The objective of the Intelligent Network (IN) concept is to rapidly and flexibly add new services without upgrading the complicated switching systems. To realize that concept in the real telecommunication system, the systems must have an environment for the creation of new services and an architecture for execution of those services. This paper proposes an environment for service creation in advanced telecommunication systems such as the IN. The service creation environment provides means to verify the new service specifications and to create executable specification. To facilitate the verification as well as to model the system resources, the service specifications are formally described by means of High-Level nets, Coloured Petri nets (CP-nets). Specifying services in CP-nets gives the capability for modeling many kinds of systems resources over the network. Especially colour plays effective roles to define both the executer of services and resourses clearly. Since IN architecture allows customers to define their own services, it is difficult to verify the services defined by different customers. Therefore, it is important to define the customers services formally at the specification level. The verification method in this paper is based on the pure net analysis technique. It is, however, extended to handle CP-nets. A customized service is verified for the integration with other services and with other customers' services. The verified services are called Service Scenarios. A software architecture in which services can be executed is also discussed. The system consists of Scenario Database, Scenario Interpreter, and Functional Execution. By simulating the service scenarios, the customized services are executed.

For fixed initial and destination states (i.e., markings), M0 and Md, there exist generally infinite firing count vectors in a Petri net. In this letter, it is shown that all fundamental particular solutions as well as all minimal T-invariants w.r.t. firing count vectors are needed to express an arbitrary firing count vector for the fixed M0 and Md. An algorithm for finding a special firing count vector which is expressed by using the only one specified fundamental particular solution is also given.