Towards a formal semantic base for the type models of the unified modeling language

In order to rigorously analyze the structure and behavior of object-oriented (OO) models, a firm semantic base needs to be developed for the OO concepts. The Unified Modeling Language (UML) is fast becoming the de facto OO modeling language, thus it is important that it have a formally defined semantic base. In this paper we discuss some early results of our efforts to formalize the UML using the Z formal notation. This paper illustrates the application of our recently developed rules to non-trivial UML type structures. The non-trivial type structures considered include combinations of generalization, aggregation, and recursive structures.