An automatic generation approach of B Specifications From UML Diagrams

The Transformation of UML models to B allows in one hand, automatically fusing both methods and use them in an integrated approach of rigorous, unified and practical software development. This approach starts from the expression of needs until programming passing through the design. On the other hand, it allows formal analysis of UML models in order to identify and correct errors, ambiguities, omissions and inconsistencies at the beginning of the development process via the B tools such as AtelierB. This paper proposes a solution to the UML graph transformation problem to B based on the graph grammar. The meta-modeling tool AToM³ is used to automate this process. A case study is presented to illustrate our approach.