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.
UML statechar B specification composite state diagram ZigBee
Li Tao Fengsheng Jia Shuaijun Yao
School of Mechanical Engineering Northwestern Polytechnical University Xian,China
国际会议
秦皇岛
英文
1658-1663
2015-09-18（万方平台首次上网日期，不代表论文的发表时间）