Research On Generation Of UML Mechanized Semantics Based On Model Transformation

Unified Modeling Language(UML) is the most popular modeling language, which is used in the design phase of software development. UML models are of vital importance to the development of software. Despite the wide use of UML, the correctness of UML models can’t be verified due to the lack of precise semantics.Mechanized semantic is a kind of formal semantics, it can eliminate the ambiguity of semantic specification defined in natural language or graphic language, and it can be defined and verified in the theorem prover. As long as the mechanized semantics of UML models is defined, UML models can be analyzed and verified in the theorem prover. However, the mapping rules between UML and the built-in language of theorem prover is hard to define, and the efficiency of manual transformation is usually low. In addition, the correctness of the transformation results can not be guaranteed.Our work focuses on generation of the mechanized semantics of UML State Diagrams and Sequence Diagrams. In order to generate automatically and improve the efficiency of the transformation, we use model transformation technology to complete the meachnical semantics generation of these two UML diagrams. Model transformation can transform UML models into formal languages automatically. We design the mapping rules between the two UML dynamic diagrams and Coq formal specification at meta-model level, and achieve to describe different UML diagrams in the same formal language. We design transformation tools from UML State Diagrams to Coq in three typical technical routes respectively, and present the implementation framework and algorithms for each route. Based on the transformation work for UML State Diagrams, we present some questions need to be answered, when developers are choosing a tool to address a particular problem, and suggest a number of concrete criterion to answer each question. Based on these questions and criterion, we analyze and compare the three routes and find out the best route for the transformation of UML dynamic diagrams. Then, we finish the transformation algorithm and prototype tool from UML Sequence Diagrams to Coq using the best route.The mechanized semantics of UML State Diagrams and Sequence Diagrams lay the foundation for further verification, and has been used in our related work. The mapping rules and prototype transformation tools that we design, simplifies the work of transforming UML dynamic diagram models to Coq specification. So developers can focus their attention on modeling and verifying. In addition, the comparison of the three technical routes and the presentation of criterion, developers can select a most suitable technology or tool to address a particular problem.