A Reverse-Engineering Approach to Understanding B Specifications with UML Diagrams

Formal methods are nowadays the most rigorous way to produce software. However, the existing formal notations are not easy to use and understand for most people. Our approach proposes to circumvent this shortcoming by producing complementary graphical views on the formal developments. This paper addresses the graphical representation of formal B specifications using UML diagrams. A reverse-engineering approach is proposed to generate several class diagrams showing the static aspects of the B developments. These diagrams can help understand the specification for stakeholders who are not familiar with the B method, such as customers or certification authorities. A concept formation technique based on weighted link matrices is proposed to improve automation