Study On Formal Method In UML Sequence Diagram And Statechart

Unified Modeling Language (UML) is a graphical modeling language with intuitionistic meanings and powerful ability for description. It provides various diagrams to depict system characteristics and complex environment from different viewpoints and different application layers.The UML syntax is defined formally, however the UML semantics is described in natural language. As a result, there are frequently ambiguity and vagueness in UML specifications. Therefore, the formal semantics study for UML can improve the veracity, consistency, and extendibility of the language.UML 2.0 sequence diagrams are always used to describe the concurrent systems and the object's dynamic interactive behaviors with the emphasis on expressing the time sequence of messages exchanges. It is able to describe its semantics with appropriate temporal logical languages. XYZ/E is an executable linear temporal logical language, which can represent both dynamic behavior and procedure features. Formally specified by XYZ/E, sequence diagrams can be analyzed under the unified temporal logical framework. The paper proposes an improved syntax definition of sequence diagram, as well as studies the semantics of sequence diagram described by XYZ/E. After analyzing the existing problems, an improved solution is proposed, which can describe the semantics of sequence diagram more exactly, based on the given syntax definition.UML can describe models from different views and at different abstraction levels. A consistency problem may arise due to the fact that the different views have information redundancy, for instance, sequence diagram and statechart have overlap aspects when they are used to model dynamic actions. Firstly, the paper mainly introduces the principles and characteristics of model checking based on formal method. It also introduces the model checking tool SPIN, including its principles and syntax. Secondly, this paper proposes an approach to analyze sequence diagram which has many different logical semantics, and a new semantics definition is given. Thirdly, a more general syntax definition of statechart is proposed. Then to deal with the hierarchy structure of statechart, finite state automata is used in this paper, as well as an automata decomposition algorithm FSADA is proposed to get an automata tree. Finally, a new model consistency criterion of sequence diagram and statechart, a new structure of Promela code ,as well as an algorithm ATTP that can convert statechart to Promela code are proposed. Model consistency is checked between sequence diagrams and statecharts with the model checker SPIN.