Exploring UML Refinement through Unification

One way of making UML more suitable for the development of critical systems is to define a formal notion of development (or refinement) for it. We explore refinement indirectly: through unification. Different UML diagrams may contain information on the same system element, which may or may not be contradictory. Such diagrams may be part of the same UML model, or taken from different models representing ''viewpoints''. A representation of the combined information of diagrams is a unification. Implicit in this is a notion of ''information content'' which needs to be formalised. A unification is not only a representation of combined information, it also witnesses consistency between the models. The theory of consistency and unifications for viewpoint specification is well-developed for formal methods. In general, such unification methods are parameterised by a notion of refinement (i.e., how to compare information content), and a notion of correspondence (relating the information between specifications). In particular, in Z all of these can be expressed syntactically, and a variety of refinement relations have been developed inspired by different styles of viewpoint specification. This paper considers a number of small UML models, their intuitive ''unifying'' diagrams, and how these would relate to the unifications of formalisations of the original diagrams. In this way, desirable properties for a formal development notion in UML emerge.