Formal semantics of UML state diagram and automatic verification based on Kripke structure

If UML is formalized with dynamic semantics, automatic verification can be performed for system model in the early stage of software procedure. It becomes more and more important to apply model checking in UML, such that software architecture can be formalized with dynamic semantics. We explicitly proposed the mapping rules between UML state diagram and Kripke structure semantics. UML state diagram is mapped to the value transition of variable rather than the transition of states, thus the situation in that system finite state automata can´t be exhausted can be resolved. Finally, a critical resource competition example is illustrated according to the theory. The mapping rules we proposed are bi-direction, as a result, the theory can be applied in both forward software engineering in design phase and reverse software engineering in implementation phase.