Research On Model Checking UML Statecharts And Tool Implementation

Being an industry standard of software modeling language, UML is well accepted and extensively used in the industry. The UML statecharts describes some dynamic behavior of a system in its lifecycle. With systems to be modeled using UML statecharts becoming more and more large and complex, the UML statecharts often contain unexpected hidden dangers. It is then necessary to check the consistency and correctness. The most popular way to check the UML statecharts is to translate the UML statecharts to a medial language as XML file, and then translate the medial file to the input language of model checking tool like Spin and SMV. My paper implements formal analysis on a subset of UML statecharts which contain hierarchy and concurrent states and enough for ordinary requirement, and then analyzes the detailed syntax and semantic of all the elements in the subset. Through the formal analysis, the paper exports the formal definition for statecharts, based on the formal definition the paper propose a new method to check statecharts, which contains statecharts mountain algorithm and transition extraction algorithm.Statecharts mountain algorithm is used for translating the UML statecharts to XML file, it changes the flat statecart to the 3D statecharts, based on the change, we extend the semantic of state and transition, the state have a new attribute named floor, which stands for the structural location, and all the states in a statecharts can be divided based on the floor; transition have a new attribute named track, which stands for the transition's movement path, and all the transitions in a statecharts can be divided into four kinds: flat, climbing up, climbing down and climbing down and then up. We can generate the enter set and exit set of transition by statecharts mountain algorithm,and then export the right XML file.Transition extraction algorithm is used for translating XML file to Promela file. Previously all algorithms used state as unit of translation, but my paper use the transition as the unit, and corresponds transitions to recursion module of the Promela code. Because statecharts' state is static and the transition is dynamic, extracting transition is more reasonable. About the statecharts events, my paper models event queue as an FIFO queue, and combines the event queue module and extracted transition module into main module, and finally implements the run-to-completion step semantic.SC2Spin implements the translation using statecharts mountain algorithm, transition extraction algorithm and event queue, user need to add the variable definition and initialization, and the Spin can check the deadlock and LTL formulas.