Formalizing the UML class diagram using Object-Z

To produce a precise and analyzable software model, it is essential for the modeling technique to have formality in the syntax and the semantics of its notation, and to allow rigorous analysis of its models. In this sense, UML is not yet a truly precise modeling technique. This paper presents a formal basis for the syntactic structures and semantics of core UML class constructs, and also provides a basis for reasoning about UML class diagrams. The syntactic structures of UML class constructs and the rules for developing a well-formed class diagram are precisely described using the Z notation. Based on this formal description, UML class constructs are then translated to Object-Z constructs. Proof techniques provided for Object-Z can be used for reasoning about these class diagrams.