Formal specification and design of intelligent network services

With the introduction of intelligent networks (IN) which will eventually allow service subscribers and network operators to introduce (develop and create) new services directly into the network, it is necessary to provide preventative measures to avoid introducing problems into the network along with the new services. One of such measures is through the use of formal methods to specify and design IN services. Formal methods allow unambiguous specification and formal analysis (and verification) of services and service elements. This is particularly important considering for instance, a set of functional components (FC) that may be used by a number of parties and therefore the interpretation of the `meaning and behaviour´ of the FCs should be precise and accurate. This is particularly so if some FCs are eventually going to be standardised and used as `off the shelf´ basic building blocks for creating new services. Moreover, without formally specifying services and service elements, it will be very difficult, if not impossible, to prove or verify the correctness of the design as well as analysing other properties of services such as features interaction. This paper presents a service specification and design methodology and describes the use of LOTOS as a formal model to represent services