The state machine formalism in UML is used for modeling discrete behavior of various system elements.Its rich notation provides a powerful description mechanism which meanwhile decreases modality of its structure and increases verifying complexity.Model checking is a technique for automatically verifying finite-state concurrent systems.By model checking the behavior of various system elements described by SM

we can find design errors as soon as possible.This paper defines an operational semantics for SM using Kripke structure in order to model checking SM.Different from existing SM semantics definitions

this paper takes undetermined factors in SM into consideration.SM is translated into kripke structure that describes all possible evolving traces on which model checker checks.