B Formal Modeling Based on UML Statechart

The combination of dynamic model and static model in UML can ensure the integrity of state information and unification of transition process. Our goal is unlimited by areas or tools to formalize the state chart by B. We build static model of state chart diagram by extracting the meta-class as the static aspects. Every meta-class of state chart can be formalized as an associated abstract machine and the state chart is formalized as an independent abstract machine. The two machines form a complete B model of state chart by calling mechanism. We transform independent elements of state chart to B and classify the state chart to simple state diagram, sequential composite state diagram and concurrent composite state diagram. By presenting the model and transition standard of every state chart, we study our method and give the example of ZigBee to verify our method.