Based On Temporal Logic Uml Interaction Model Checking

UML (Unified Modeling Language) is a visible modeling language, which is easy to comprehend and easy to describe. UML provides kinds of modeling elements to describe the property, function and running environments of software system from different view points of the system. The analysis and design of software system based on UML has been widely used in different fields. UML Interactions describe the interactive behaviors of software systems detailed and precisely, which provide a convenient and high-efficient visible model for the developers and end users to help them comprehend the interaction behaviors of the system correctly. It has become a very important research filed that checking UML interaction models to judge whether the model derived from software systems satisfies the properties.Model checking is a widely used formal automate verification technology. It verifies the modal or proposition properties of the system through the search of states explicitly or computing fixed points. This paper describes my research on the model checking UML 2.0 interaction models with the temporal logic under the framework of automaton theory.In order to check the properties of UML 2.0 interactions models, I formally describe the interactions and transform them to an automaton which can accept message exchanges or state changes of system. The paper abstracts the grammars and semantics of interactions, describes the basic grammars of interactions with BNF, and put forwards an interactive automaton, which is a Buchi automaton, to describe interactions formally, based on the visible grammars of interactions published by OMG.Then, the paper investigates the model checking method to verify the properties of UML interaction models with interactive automaton and the temporal logic, and presents the Marking algorithm for model checking. This algorithm judges whether the UML interaction models designed by users satisfies the property and the standard of the software system, by marking all the states of interactive automaton, and checking the value of the CTL formulas of each state.