Stefan Gossens
Inhaltsangabe:Abstract: The use of formal methods in the area of software specification is a subject of current software engineering research and becoming increasingly accepted by a larger audience in the computer science community. However, the specification of telecommunication networks is mainly based on weakly formalized paradigms that rely on natural-language descriptions of the behaviour of network components. The research focus of the GDMO project, in the context of which this paper originates, was the introduction of elements of formal specification into such specification methods. This paper explores procedures to translate specifications in the semi-formal network component specification formalism GDMO (Guidelines for the Definition of Managed Objects), defined and standardized by ITU and ISO, into ZEST, an object-oriented extension of the formal Z specification language. It also contains an illustrative case study of the translation of an application-sized GDMO specification into ZEST. Inhaltsverzeichnis:Table of Contents: I.Introduction1 1.The GDMO Project3 2.The OSI Network Management Paradigm5 2.1A Reference Model for Network Management5 2.2GDMO: A Notation for the OSI Network Management Paradigm8 3.The Xcoop System11 3.1Providing Connections over Network Boundaries: An Important Issue of Modem Telecommunication11 3.2Establishing Long-Distance ATM Connections12 3.3ATM Basics13 3.4The Xcoop Philosophy15 4.Z and its Object-Oriented Extensions19 4.1Z19 4.2Object-Orientation in Z21 II.Translating GDMO to ZEST29 5.Translation 'Frontend': Inferring an Object Model from GDMO Specifications31 5.1Outline31 5.2Relations in GDMO33 5.3Considerations on ASN.135 5.4Building an Object Model38 5.5Example of Relation Inference Using Algorithm 147 5.6Discussion of the Approach50 6.Translation 'Backend': Translation of GDMO to ZEST53 6.1Overview53 6.2Translation of ASN.1 Syntaxes into ZEST Fragments54 6.3Translation of GDMO to ZEST63 6.4C