Research On Formalization Of UML Sequence Diagrams

UML Unified Modeling language is developed from variety of object-orientedmodeling method. It has explicit concepts, clear graphic structures and concisemodeling methods. Also, it is easily understood and used, do not depending specificsoftware development process. So, in 1997, it is considered as specification ofmodeling language by OMG (Object Management Group), gradually becomingpractical industrial standards.In fact, UML is semi-formalization. Its syntax structure adopts formalizedspecification and semantics are described by non-formalization nature language.This makes UML lack precise and formalized semantics. As a result, related toolscan only support to check its syntax. However, they can not analyze and inspect theaccuracy and consistency of the model. These factors above could give rise to usinga wrong design model and reducing efficiency and quality in the softwaredevelopment. What's more, they could break down the whole software projects.Formal methods, which is based on rigorous mathematical reason, is a kind of is aprecise, unambiguous rule for formal specification and provides rigorousmathematical foundation for exactly understanding model. The features of formalmethods are very valuable for automatic code generation and reliable softwaredevelopment.In this paper, UML sequence diagram is the research object. In order to improvethe accuracy of the semantics of UML sequence diagrams, this paper studies theformalization of UML sequence diagram using the approach which combines thefeatures of description logic and computation tree logic.Firstly, the previous research work on UML formalization is summarized,compares the similarities and differences of various formal methods, analyzes theways in which the deficiencies and shortcomings, and describes the opinion of theauthor's views. Secondly, both description Logics and CTL exist insufficient inknowledge representation. To solve the problem, this paper proposes a solution bytranslating the UML sequence diagrams into a formalization system ALCQI-CTLwhich combines the features of description logics and CTL, and then describing theformal method in detail. Lastly, the formal method is used to formalize the UMLsequence diagram, which demonstrates the formal method is feasible.