Research On Bi-Transformation Between UML Models And Formal Models

The Unified Modeling Language (UML) provides a graphical notation to express the design of object-oriented software systems and has become the de facto industry standard for software design. However UML lacks precise semantics and is semi-formal. Formal specification languages are intended to provide precise and complete models for proposed software systems. Many researchers have done a lot of work in translating UML models into formal models to validate UML models. since it is impossible to verify whether an informal requirement is equivalent to a formal description,This "going back and forth" between the realms of informal and formal specification is necessary. so formal models need to be reversely transformed back to UML models.It is very easy to describe the static structure of software.In this paper, we transform UML models to formal models using the method which called "UMLTranZ". UMLTranZ can transform UML concept Class Diagram to Z models. the main structure of Z models is Schema, it can describe semantics of UML models formally. using the existing reason tool, we can analyze and reason Z models.XMI(XML Metamodel Interchange) is a format of transmitting model data, provid-ed by OMG.using Transmitting Metadata Differences in XMI, we propose a method of reverse transformation from formal models to UML models. this reverse transformation is a indirect transformation, it can undos the weaking effects of transformation from UML models to formal models. integrating this reverse transformation with the existing trans-formations, we can achieve the target of Bi-transformation between UML models and formal models.We also testify the feasibility and correctness of the reverse method by Unifying Theories of Programming (UTP). According of Z models transformed by UMLTranZ, we define the rules of reverse transformation from Z models to UML models based on the First Order Logic and Set theory. using the rules, we can reversely transform Z models to UML Class Diagrams. integrating this reverse transformation with UMLTransZ, we can achieve the target of Bi-transformation between UML and Z.At the end of the paper, we design a tool of Bi-transformation and develop a proto-type with Java.