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.


Formal Method Class Diagram Building State Concrete State Open Building 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abrial, J.-R.: System study: Method and example (1999),
  2. 2.
    Idani, A., Ledru, Y.: Dynamic Graphical UML Views from Formal B Specifications. Journal of Information and Software Technology 48(3), 154–169 (2006)CrossRefGoogle Scholar
  3. 3.
    Idani, A., Ledru, Y.: Object Oriented Concepts Identification from Formal B Specifications. Journal of Formal Methods in System Design 30(3), 217–232 (2007)CrossRefGoogle Scholar
  4. 4.
    Idani, A., Ledru, Y., Bert, D.: Derivation of UML Class Diagrams as Static Views of Formal B Developments. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 37–51. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  5. 5.
    Laleau, R., Mammar, A.: An Overview of a Method and Its Support Tool for Generating B Specifications from UML Notations. In: 15th IEEE Int. Conference on Automated Software Engineering, pp. 269–272. IEEE CS Press, Los Alamitos (2000)Google Scholar
  6. 6.
    Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Sekerinski, E.: Graphical Design of Reactive Systems. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 182–197. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  8. 8.
    Snook, C., Butler, M.: U2B − A tool for translating UML-B models into B. In: Mermet (ed.) UML-B Specification for Proven Embedded Systems Design (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Akram Idani
    • 1
  1. 1.Laboratoire d’Informatique de GrenobleSaint Martin d’Hères cedexFrance

Personalised recommendations