Research Of UML-Oriented Model Checking

Unified Modeling Language (UML) is a graphical modeling language with powerful ability and intuitionistic meaning. It provides various diagrams to depict system characteristics and complex environment from different viewpoints and different application layers. UML-based software developing process and modeling environments have been widely accepted in the industrial community, which includes the safety areas such as spaceflight, national defense, and automobile, etc. Verifying if UML models satisfy the requirements has become a key issue.Model checking is an important technology of automatic verification. UML Statecharts depicts the behaviors and states of an object in its life cycle, and acts as an important role in software analysis and modeling. An approach of model checking UML Statecharts is presented in this paper. Firstly, UML Statecharts is structurally expressed by Extended Hierarchical Automaton (EHA), and its operational semantics is expatiated. The correctness of semantics can be ensured through finding the maximal non-conflict transition set. The characteristics and forms of describing properties of UML models with linear temporal logic are also studied. After-transforming the labeled transition system of operational semantics and linear temporal logic formula into Btlchi automata respectively, the correctness of UML Statecharts can be verified using automaton-based model checking method.Because of state explosion and the complexity of semantics, model checking UML Statecharts is restricted by the software scale and the refinement degree of design specification. We define a set of dependence relations through analyzing the characteristics such as hierarchy, concurrent and synchronization in EHA. The algorithm of slicing EHA from the slicing criterion composed of states and transitions is presented. When slicing criterion is extracted from the property to be verified according some rules, the sliced EHA and the original one are equivalent to the property. Slicing can remove the irrelevant hierarchies and concurrent states to the property, reduce the state space, and help analyzing and understanding the models.UML collaboration diagrams describe the dynamic interactions and associations among the objects in concurrent multi-object system. We present the composition methods for asynchronous and synchronous systems respectively, which are modeled by UML collaboration diagram and Statecharts. These methods can be used to verify the properties of whole system. To reduce the state explosion caused by concurrent objects, we study the compositional verification of synchronous UML models based onsynchronous composition and simulation relation between structures. It makes possible that system can be verified without constructing the global state transition diagram. Furthermore, we make use of the hierarchies in compositional verification, which makes it possible to substitute some components of implementation with abstract specifications (which usually have smaller state space).We have designed and implemented an UML-based model checking tool, UML-MC. It can verify the Statecharts modeled by Rational Rose or I-Logix Rhapsody. The counter-examples will be given when system does not meet the properties. Furthermore, we design an UML-based software testing and verification environment based on the researches of UML testing and verification, and implement the prototype.