The Formal Semantic Study Of UML State Machine

As a de facto object-oriented modeling standard language, the complexity and magnitude of UML(Unified Modeling Language) is inevitable. However, it also contains a lot of standard elements with vague and sparse semantics. In the UML specification, the editors describe the static semantics in formal language OCL (object Constraint Language) and natural language, while the dynamic semantics is almost described in natural language. UML lacks in a strict definition of dynamic semantics. Therefore, the formal semantic study of UML is helpful for the improvement of the clarification, equivalence, consistency, and extendibility of the language, thus offers a powerful theoretical tool for the validity proof, transition of the model and the consistency check of the modeling tools supporting UML.At present, many organizations and individuals are engaged in the study of UML formal semantics. They attempt to influence the future of UML through the study of UML. The methods which these organizations and individuals use are mainly supplemental approach and OO-extended formal language approach. Both of the approaches have their own advantages and disadvantages. Because the formal language in supplemental approach don't have the object-oriented feature, using supplemental approach makes it difficult to integrate with the present practice. While the way of OO-extended formal language approach can't directly formalize the semantics of UML model, which affects the readers' understanding of UML model rbrmalization.Based on those disadvantages, the author combines the two methods and puts forward a new way of formal state machine semantics. That is, firstly, analyze the grammar structure of the metamodel of UML state machine. Then through RAISE (Rigorous Approach to Industry Software Engineering) which has object-oriented features directly formalize the operating semantics of UML state machine. In the part of grammar structure analysis, the author puts forward a state hierarchical structure which analyzes all the states of UML state machine and the relationship between themand then analyze the structure of the events and transitions in turn and finally get a summarizing formal description of the grammar structure of UML state machine. In the semantic formalization of run to completion step, using RSL, the author in turn formalizes semantics of the enabled transitions, conflicts of transitions, solution of conflicts, and the selection of transitions, and finally puts forward a algorithm of the run to completion step in UML state machine. Combining those two parts, the author puts forward a new complete formal method of the semantics of UML state machine.At last, the author uses an example to show that using the formal description of UML state machine semantics can justify the important properties of those systems described by UML.