Research on Model Checking Technology of UML

To checking the correctness of UML models, we integrate UML and Model Checking effectually in software development. At the beginning, we select class diagram, state diagram and collaboration diagram from UML models to define a system description model, verification model and system constraints. Following, 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 then verifies the correctness of models with SPIN. Finally, we conduct research on an example, and the experiment result proves the correctness of this method.