Research On The Mechanical Semantics And Attribute Verification Of UML Class Diagram

As a current mainstream modeling language, Unified Modeling Language (UML) is a universal graphical modeling language extensively applied to various stages of software life cycle. Straightforward and easy to understand, UML has support from relatively good visualization tools (such as Rational Rose, Argo UML, etc) and it is widely used in model driven engineering. Additionally, it is an industrial standard facing object-oriented analysis and design. However, the current UML2.0 uses semi-formal diagrams, constraints and non-formalized natural language texts to describe. Due to the lack of rigorous formal semantics and formal specification definition of the model refinement relationship, it cannot guarantee the accuracy and consistency in the process of UML modeling. The absence of precise formal semantics may lead to the following problems:(1) Inconsistency of comprehend the model, namely that different people will have different understandings of the same model; (2) It is hard to validate and analyze the model to ensure its correctness.The paper mainly focuses on the mechanical semantics and the property verification of the UML class diagram. The main content of the paper is to extract the formal specifications from UML class diagrams by defining the basic elements of the class diagrams. The theorem prover Coq is used to make formalized description of the formal specifications and elaborated operations of the UML class diagrams, providing the semantic foundation for the subsequent verification of system properties, model refinement, etc. Based on the above formal description, the significant attributes and the refinement relation of the UML class diagrams are converted into mathematical theorems which will be formally defined and verified in Coq. And the provability of the theorems shows the correctness of the system properties and the refinement relation. The above method not only makes up for the deficiency of the UML but ensures the validity and the consistency of the UML model and its refinement, which provides a theoretical basis on the verifiable framework of the software design model elaboration. In addition, according to the formal expression of the basic elements of the UML class diagrams, the paper also defines the relevant mapping rules. And the paper uses Kermeta, the meta-model transformation plugin of Eclipse, realizing the automatic generation from the graphical modeling of class diagrams to its formal description. Therefore, the developers can concentrate on system modeling, analysis and verification without having to worry about the complicated conversion process.