Service Extension at the Specification Level

Abstract

This report illustrates some techniques for extending a formal specification of a system in order to add new service features to the system. The system in question is a PABX and the new service features are: abbreviated dialling, call diversion, call holding and forwarding and, a call-back facility. A state-based approach is taken in the formal specification using the Z notation. Two main extension techniques are used: adding a new operation and adding a new state component. The aim is to use as much of the existing system as possible when providing these new services. Promotion of various forms of reuse is seen as important. Extensive use is made of the Z schema calculus.