Authors: Akram Idani
Tags: 2009, conceptual modeling
While formal methods are focused on some particular parts of software systems, especially secure ones, graphical techniques are the most useful techniques to specify in a comprehensible way large and complex systems. In this paper we deal with the B method which is a formal method used to model systems and prove their correctness by successive refinements. Our goal is to produce graphical UML views from existing formal B specifications in order to ease their readability and then help their external validation. In fact, such views can be useful for various stakeholders in a formal development process: they are intended to support the understanding of the formal specifications by the requirements holders and the certification authorities; they can also be used by the B developers to get an alternate view on their work. In this paper, we propose an MDE framework to support the derivation of UML class and state/transition diagrams from B specifications. Our transformation process is based on a reverse-engineering technique guided by a set of structural and semantic mappings specified on a meta-level.Read the full paper here: https://link.springer.com/chapter/10.1007/978-3-642-01862-6_20
