Service Specification Using Z
Michael J. Butler, Mícheál Mac an Airchinnigh · ePrints Soton (University of Southampton) · 1993
Z is a formal description language based on set theory and predicate logic [12].In SCORE, we have investigated, through a number of case studies, how Z may be used to support service creation.Z may be used in the specification stage of service creation as it provides a succinct and unambiguous way of specifying services.Experience has shown that formal notations such as Z may also be used to aid the requirements gathering stage of the service creation process; by building partial formal models based on requirements, these requirements can be clarified and further elaborated before a more complete specification is produced. Conceptual ModelGuidelines on the use of Z for telecoms service specification are described in this report.We have taken the view that a service is provided by a system.A standard approach to system specification was taken, whereby we focus on some clearly defined notions-entities-and build appropriate relations between them.We refer to the entities and the relationships between them as a conceptual model.The conceptual model is represented in Z using mathematical structures.Commonly used mathematical structures used in service specification are sets and functions.Functions are used to describe mappings from elements of one domain to another and are used in many different contexts.For instance, a function could be used to specify communications connections by mapping A-numbers to B-numbers, or could be used to describe a freephone service by mapping freephone numbers to real numbers, or could be used to describe the relationships between service subscribers and service providers.The conceptual model is developed by identifying entities and relationships between them from the service requirements, and gradually elaborating and refining the conceptual model by posing questions of the requirements.