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.

A requirement specification acquisition method combined with hypothesis-based reasoning and model reasoning is proposed for obtaining service specifications from the ambiguous and/or incomplete requirement specifications of communications services. Errors at an early stage of software development cost more to debug than those at a later stage. Specification acquisition is the most upstream development process. Nevertheless, the system support for specification acquisition is delayed compared with other development phases.' Users do not always have precise requirements. It is therefore inevitable that user requirements contain ambiguities, insufficiencies and even contradictions. Considering this, it is indispensable to support a specification completion method that derives service specifications from such problem requirements. This paper proposes a combined method to obtain consistent and complete specifications from such problem requirements. Communications service specifications can be described by specifying terminal behaviors which can be recognized from outside the communications system(s). Such specifications are described by a rule-based language. Requirement specifications usually have components that are ambiguous, incomplete, or even contradictory. They appear as rule description and/or missing rules. From such requirements, service specifications are obtained by using hypothesis-based reasoning on input requirements and existing service specifications. When existing specifications cannot be used to obtain complementary specifications, a communications service model is used to propose new rules. The proposed methods are implemented as a part of a communications software development system. The system enables non-experts in communications systems to define their own service specifications.