Research On Verification Technology Of UML Models Based On Model Checking With SPIN

As the representative of object-oriented methods of software analysis and design, UML (Unified Modeling Language) has drawn extensive attention from the research field and has been studied and applied in various fields. However, as a popular symbolic modeling language in which its semantics is described in natural language, UML is lack of precise semantics. Accordingly, it is difficult to analyze and verify UML models when we want to examine whether the specification of design has conformed to the expected requirement or not. Model Checking is an automatic verification technology which can considerably guarantee the trusted property of system and has been applied in the industrial field widely. Thereby, it has become a hotspot in the software engineering domain to investigate how to integrate UML and Model Checking effectually in order to avert mistakes in system modeling and to enhance the productivity and quality of softwares.SPIN (Simple PROMELA Interpreter) is a type of open source tool of model checking. It has been applied in industrial and academic fields for occupying small memory space and high efficacy in guaranteeing that the program can be verified according to its original working process. Hereby, the present paper chiefly researches the verification technology of UML model based on model checking with SPIN. At the beginning, the present paper introduces the formal verification methods, reviews the theory, traits and process of model checking technology, and elaborates the theory of the model checking tool—SPIN, the input language PROMELA and the optimization technology. After that, the present paper analyzes the structure and feature of UML models, and selects class diagram, state machine diagram and collaborations diagram from UML models as a system description model, and then combines class diagram and state machine diagram into a verification model in order to meet the needs of model checking. Following that, based on the homomorphic mapping method, this paper proposes a method for transforming the UML verification model to PROMELA model, uses the Hierarchical automata to describe the state machine and defines its formal semantic, and translates the verification model including the information of state machine diagram and class diagram into a corresponding PROMELA model. Meanwhile, this paper assigns the LTL formulas attained from the informatiom of the collaboration diagram of UML as system constraints, and then verifies the correctness of the system modeled by UML models with the model checking tool—SPIN. Finally, based on the above work, this paper develops a tool of UML model automatic transformation and verification—UML2PROMELA.