A Generic Process and its Tool Support towards Combining UML and B for Safety Critical Systems.

Abstract

The complex requirements of software systems justify the use of the best existing techniques to guarantee the quality of specifications and to preserve this quality during the programming phase of a software life-cycle. On the one hand, visual specification languages (such as UML) have been widely used for specifying, visualizing, understanding and documenting software systems, but they suffer from the lack of precise semantical basis. Hence, these languages are practical for large-scale information systems rather than for industrial applications which address safety challenges. On the other hand, formal methods (such as B) are specifically used for safety critical systems in order to rigorously check their correctness but they lead to complex models which may be difficult to read and understand. These complementarities between formal and graphical techniques motivate our aim to develop a tool for combining both methods starting from UML and producing B models. Existing works which tried to integrate UML and B proposed model-to-model transformation techniques which miss a clear and explicit conceptual foundations. In order to circumvent this shortcoming we propose a metamodel-based transformation technique which is founded by a set of structural and semantic mappings between UML and B. A reusable and evolutive framework is then developed to assist derivation of formal B specifications from UML diagrams.