More and more large systems are taking UML as requirements description language for system analysis and design, especially in those safety-critical systems. One of the most important dynamic behaviorspecifying mechanism of UML---the UML state machine, is widely used for specification of communicationprotocols and control units. Unfortunately, UML has no strictly defined formal dynamic semantics. It is difficult to do formal verification and proof on the requirements. In this paper, a formal semantics of UML state machine is built. The UML state is firstly represented by inductive state term from some kind of term algebra. Secondly, a labeled transition system (LTS) is introduced, in which an LTS-state is a UML state term, an LTS-transition is a micro step of UML state machine. In the end, a set of Plotkin-style structural operational semantics (SOS) rules inductively defines a compositional formal semantics for UML state machine. This method not only synthesizes those formal methods for classical Statecharts, but also makes innovation addrerssed to UML state machine. At any tiem, the configuration of the machine can be inferred from the state term. The simplified LTS-lable and structuralized operational semantics ruls will play a fundamental fole in formal verification.