Translation of GDMO to ZEST

Diplomarbeit von Stefan Gossens

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.

Table of Contents:

I.	Introduction	1
1.	The GDMO Project	3
2.	The OSI Network Management Paradigm	5
2.1	A Reference Model for Network Management	5
2.2	GDMO: A Notation for the OSI Network Management Paradigm	8
3.	The Xcoop System	11
3.1	Providing Connections over Network Boundaries: An Important Issue of Modem Telecommunication	11
3.2	Establishing Long-Distance ATM Connections	12
3.3	ATM Basics	13
3.4	The Xcoop Philosophy	15
4.	Z and its Object-Oriented Extensions	19
4.1	Z	19
4.2	Object-Orientation in Z	21
II.	Translating GDMO to ZEST	29
5.	Translation 'Frontend': Inferring an Object Model from GDMO Specifications	31
5.1	Outline	31
5.2	Relations in GDMO	33
5.3	Considerations on ASN.1	35
5.4	Building an Object Model	38
5.5	Example of Relation Inference Using Algorithm 1	47
5.6	Discussion of the Approach	50
6.	Translation 'Backend': Translation of GDMO to ZEST	53
6.1	Overview	53
6.2	Translation of ASN.1 Syntaxes into ZEST Fragments	54
6.3	Translation of GDMO to ZEST	63
6.4	Considerations Concerning Notifications	70
6.5	Discussion of the Approach	73
6.6	Related Work	74
7.	Case Study: Translation of the Xcoop Model	79
7.1	Applying the Translation Scheme to the Xcoop Specification	79
7.2	Exploring the ZEST Xcoop Specification	83
7.3	Summary	94
8.	Conclusions	97
8.1	Summary: GDMO and ZEST	97
8.2	Pros and Cons of the Translation Approach	100
8.3	Outline of a Translation Tool	101
A.	ZEST Specification of the Xcoop model	109
A.1	Index to the Specification	110
A.2	Specification Text	113
	Abbreviations	153
	Index	155