Statecharts is widely used as a behavioral modeling language for reactive systems for its concise and intuitive expression. It can represent the system behavior at different levels of abstraction, and therefore can represent the result of every refinement step in the process of system modeling. However, it’s beyond its capability to reason about whether the model semantics of the lower level preserves that of the higher level and whether the models they describe satisfy some properties. In this aspect, the formal language XYZ/E can be used complementarily. The XYZ/E is an executable linear temporal logic. It can express both the properties and behavior of systems. In this paper, the semantics of Statecharts is defined inductively using the Basic Transition System, and its temporal semantics is expressed by an XYZ/E formula. The semantics we give is modularly compositional. The semantic preserving of different refinement steps can be guaranteed by the semantic definition directly. Models that Statecharts specify and their properties are represented in the same logic, so the assertion that a model meets its specification is expressed by logical implication.