Unwed Modeling Language (UNIL) has been widely used in software development. Verifying whether a UML model meets the required properties has become a challenge. Model checking is an iinportarit technology of automatic verification to ensure the correctness of designed models. Because of space explosion and complicated semantics

model checking Statecharts are restricted by the sofrware scale and the refinement degree of design.In this paper

UML Statecharts are structurally expressed by Extended Hierarchical Automaton (EHA). A set of dependence relations is specified after analyzing the characteristics such as hierarchy

concurrency and synchronization in EHA. The algorithm of slicing EHA based on the slicing cilterion which is composed by states and transitions is presented.The sliced EHA and the original Statecharts are equivalent to the property.The algorithm removes the hierarchies and concurrent states which are irrelevant with the property

and reduce the state space efficiently.