Service specification verification and validation for the intelligent network

New architectures of telecommunications networks like the Intelligent Network (IN) proposal allow an ever easier way to introduce new services into a network. However, this facility and the short delays that can be achieved between the first informal specification of a service and its deployment appeal for automated validation methods to gain confidence in the new services before they are actually introduced. In this thesis, the usage of an object-oriented methodology is advocated for the specification of telecommunications services. Such methodologies are better suited to the needs of service specifiers. Therefore it is proposed to specify telecommunications services with the object-oriented analysis method Fusion. However, the notations defined by the Fusion methodology are not formal enough to allow an automated validation of the specification. Therefore these notations are extended and formalized to obtain a language called FUS++. A FUS++ specification contains two parts: A "constructive" part which defines the behavior of the specified system. The semantics of this part can be expressed with an extended finite state machine (EFSM). A "property-oriented" part which contains properties that must be satisfied by the specified system. These properties are expressed in linear time temporal logic (LTL). Special constructs were added to FUS++ in order to allow an easy merging of services that where specified independently. The semantics of these new constructs is based on the mechanisms foreseen by the IN for the introduction of services in the network. Being able to combine freely services in a system allows us to address the problem of the detection of interactions between these services. Detecting problems in a specification is done during the validation phase. To validate a FUS++ specification, it is translated to Promela; the Promela program is then validated with the validation tool Spin. During this phase, one proves that the properties of the specification are satisfied by the constructive part. In the second part of this work, it is shown how the properties of a FUS++ service specification can be validated for the implementation of the service in a real intelligent network. Consequently, a mapping function is specified between the states of an intelligent network and the states of an abstract mode1 of such a network.