Formal approach to metamodeling: A generic object-oriented perspective

Abstract

Formal methods and metamodeling are promising ways to cope with the ever increasing size and complexity of modem software systems: the former should provide the means to write precise, unambiguous, and provably consistent descriptions of system properties, while the latter should lead to a better understanding of the software development process through metamodeling the descriptions produced in the course of the software development process. In this paper, we propose to use both formal methods and metamodeling, in order to combine their advantages. A generic metamodel of object-oriented systems is presented and specified, using the Z formal notation. Other known models may easily be mapped to our model, as demonstrated on the OMG core object model. The formal notation facilitates the specification of various constraints and consistency checks, a number of which are shown in detail.