Formalizing UML Models with Object-Z

The Unified Modeling Language (UML) has been developed as a standard language for object-oriented designs. Through its graphical and intuitive diagrams, software analysis and design process become easy. However, this graphical notation lacks precisely defined semantics. It is difficult to determine whether the design is consistent, unambiguous and complete. This paper provides a method of formalizing UML models. It gives the transforming rules from UML models to Object-Z constructs. With this method, the semantics of UML models are directly expressed in formal language Object-Z. The UML class, sequence and statechart diagrams are formalized using this method. A tool OZRose is developed to automate the transforming process.