Research of model checking UML
Luo Gui-ming · Journal of Computer Applications · 2007
Unified Modeling Language(UML)is the most commonly used method in software system design and analysis,and how to verify that the UML model satisfies some properties is a very important issue.Model Checking is an efficient automatic technique for the improvement of system's reliability,and this paper is a research into how to check UML model through the Simple PROMELA Interpreter(SPIN)model-checker.After describing the UML model using formal method,we first used hierarchical automata to express statecharts diagram.In addition,we translated the statecharts and part of the class diagram into PROMELA based on the operational semantic of hierarchical automata,and verified the model by using Simple Promela Interpreter(SPIN)to test if it satisfied the LTL properties.We also verified the consistency between sequence diagram and statecharts diagram by using LTL formula to express sequence diagram.Finally,based on the method,we developed a model checker tool called UMLChecker.