Transformation From UML State Machine to B Formal Specification
Chen Hai-quan · Microelectronics & Computer · 2005
Integration of formal method into high-confidence software engineering was studied. The UML state machine of software design model was first transformed into B formal specification. Then, in the B tool kit environment, the reli-able implementation model was developed according to the refinement principle of B method and its correctness verifica-tion facility. A suit of transformation rules from UML state machine into B formal model were proposed, including UML basic state diagram, hierarchical state diagram and concurrent state diagram. Experiment showed that the proposed trans-formation rules were practical.