High-confidence Embedded Software Development Based on UML State Machine and B Method
Hao Dong · Jisuanji gongcheng · 2006
A practical scheme integrating UML state machine and B method to develop reliable embedded software is proposed.The UML state machine model of software is first translated into B abstract model whose consistency is verified in B tool;then in the environment of B method,the verified abstract model is refined step by step into implementation model and finally translated into source C code with the aid of B toolkit.The correctness of the abstract model and of the refinement process is guaranteed by the B method.Experiment shows that this scheme strategically combines the advantages of UML’s intuitionism and B method’s rigor and can effectively improve the development and verification of high-confidence embedded software.The rules of transforming from UML state machine into B abstract machine are provided.