Research And Application Of UML Models Consistency Verification Based On SPIN

With the rapid development of computer technology, the software systems become more complexity. To resolve the problem of development,UML provides a family of diagrams for defining system structure and behavior. As lacking of precise formal description and semantic definition, it is difficult to guarantee the model consistency or correctness among the various views. The detection of model consistency and correctness has become a very prominent and promising research topic recently. But the existing methods mainly focus on the detection by manual review or semi-formal reasoning, which is improper in industrial applications. Model Checking is a fast and fully automated formal verification method. To address the overlapping definitions and contradictory problems between different models, this paper verifies the correctness and consistency of UML models with the help of SPIN detection tool, the main work is as follows.Firstly, considering the elements of UML class diagram, sequence diagram, activity diagram, the syntax and semantics was described in strict formal method; The consistency checking of UML models must ensure correctness of the model, in addition it's hard to resolve and achieve automatic verification for multi-level structure activity diagram. So the new method was proposed to decompose the multi-level activity diagram based on tree structure. Then the sub-diagrams are transformed to the input model of SPIN according to previous constructed model, and the Promela was executed to check the liveness and safety.Then, for the consistency problems of UML models, it defines the relationships of messages and semantic consistency of UML models. According to the relationships of sequence messages, the sequence diagram was simplified. So the transformation was carried out from sequence behavior to activity track. The process synchronization and checking algorithm was present with the analysis of Promela features. And the consistency of UML models war verified with the help of SPIN detection tool.Finally, according to the verification algorithm of activity diagram and the consistency checking algorithm of UML models, the tool was achieved with Eclipse Plug-in platform. Through the "Offensive System" experiments, the results showed that the system design tool detected the consistency of models. In addition, the inconsistency was eliminated successfully.