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 statechart by B. We build static model of statechart diagram by extracting the meta-class as the static aspects. Every meta-class of statechart can be formalized as an associated abstract machine and the statechart is formalized as an independent abstract machine. The two machines form a complete B model of statechart by calling mechanism. We transform independent elements of statechart to B and classify the statechart to simple state diagram, sequential composite state diagram and concurrent composite state diagram. By presenting the model and transition standard of every statechart, we study our method and give the example of ZigBee to verify our method.