Formal Methods in System Design

, Volume 30, Issue 3, pp 217–232 | Cite as

Object oriented concepts identification from formal B specifications



This paper addresses the graphical representation of static aspects of B specifications, using UML class diagrams. These diagrams can help understand the specification for stakeholders who are not familiar with the B method, such as customers or certification authorities. The paper first discusses some rules for a preliminary derivation of a class diagram. It then studies the consistency of the concepts preliminarily identified from an object oriented point of view. A formal concept analysis technique is used to distinguish between consistent classes, attributes, associations and operations. The proposed technique is to incrementally add operations to the formal specification which automatically result in evolutions of the class diagram.


UML Integrated methods 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
  2. 2.
    Behm P, Benoit P, Faivre A, Meynadier J-M (1999) METEOR: A successful application of B in a large project. In: Wing JM, Woodcock J, Davies J (eds) Proceedings of the FM′99: World Congress on formal methods, Lecture notes in computer science, vol 1709, Springer-Verlag, pp 369–387Google Scholar
  3. 3.
    Bert D, Cave F (2000) Construction of finite labelled transition systems from B abstract system. In: Integrated formal methods, lecture notes in computer science, vol 1945, Springer-Verlag, pp 235–254Google Scholar
  4. 4.
    Bert D, Potet M-L, Stouls N (2005) GeneSyst: a tool to reason about behavioral aspects of B event specifications. Application to security properties. In: Proceedings of the ZB2005, lecture notes in computer science, vol 3455, Springer-Verlag, pp 299–318Google Scholar
  5. 5.
    Casset L (2002) Development of an embedded verifier for java card byte code using formal methods. In: FME′02, formal methods Europe, lecture notes in computer science, vol 2391, Springer-Verlag, pp 290–309Google Scholar
  6. 6.
    Dick J, Loubersac J (1991) Integrating structured and formal methods: A visual approach to VDM. In: van Lamsweerde A, Fugetta A (eds) Proceedings of European Software Engineering Conference (ESEC ′91), vol 550. Lecture notes in computer science, Springer-Verlag, pp 37–59Google Scholar
  7. 7.
    Dupuy S, Ledru Y, Chabre-Peccoud M (2000) An Overview of RoZ: A Tool for Integrating UML and Z Specifications. In: CAiSE 2000, vol 1789. Lecture notes in computer science, Springer-Verlag, pp 417–430Google Scholar
  8. 8.
    Fekih H, Jemni L, Merz S (2004) Transformation des spécifications B en des diagrammes UML. In: Julliand J (ed) AFADL: Approches Formelles dans l'Assistance au Développement de Logiciels, pp 131–145Google Scholar
  9. 9.
    Hammad A, Tatibouet B, Voisinet JC, Weiping W (2002) From a B specification to UML Statecharts Diagrams. In: Proceedings of the 4th International Conference on Formal Engineering Methods (ICFEM′2002), vol 2495. Lecture Notes in Computer Science. pp 511–522, Springer-VerlagGoogle Scholar
  10. 10.
    Harel D (1987) Statecharts: A visual formalism for complex systems. Sci Comput Programm 8(3):231–274, ElsevierMATHCrossRefGoogle Scholar
  11. 11.
    Idani A, Ledru Y (2005) Dynamic graphical UML views from formal B specifications. Information and Software Technology Journal. Article in press. Accepted March 2005, ElsevierGoogle Scholar
  12. 12.
    Idani A, Ledru Y, Bert D (2005) Derivation of UML class diagrams as static views of formal B developments. In: Formal methods and software engineering, 7th international conference on formal engineering methods, ICFEM 2005, vol 3785. Lecture Notes in Computer Science. Manchester, UK, Springer-Verlag, pp 37–51Google Scholar
  13. 13.
    Laleau R, Mammar A (2000) An overview of a method and its support tool for generating B specifications from UML notations. In: International Conference on Automated Software Engineering (ASE2000), IEEE CS Press, pp 269–272Google Scholar
  14. 14.
    Laleau R, Polack F (2002) Coming and going from UML to B: A proposal to support traceability in rigorous IS development. In: ZB′2002—Formal specification and development in Z and B, vol 2272. Lecture Notes in Computer Science, Springer-Verlag, pp 517–534Google Scholar
  15. 15.
    Lano K (1995) Formal object-oriented development, SpringerGoogle Scholar
  16. 16.
    Lano K, Goldsack S (1996) Intregrated formal and object-oriented methods: The VDM++ approach. In: Bryant A, Semmens L (eds) Method integration workshop. Electronic Workshops in Computing, Springer, LeedsGoogle Scholar
  17. 17.
    Lano K, Houghton H, Wheeler P (1996) Integrating formal and structured methods in object-oriented system development. In: Formal Methods and Object technology, chapter 7, SpringerGoogle Scholar
  18. 18.
    Ledang H, Souquières J (2002) Contributions for modelling UML State-Charts in B. In: Integrated formal methods, 3rd international conference, IFM 2002, vol 2335. Lecture Notes in Computer Science, Springer-Verlag, pp 109–127Google Scholar
  19. 19.
    Leuschel M, Butler M (2003) ProB: A model checker for B. In: Araki K, Gnesi S, Mandrioli D (eds) FME 2003: Formal methods, vol 2805. Lecture Notes in Computer Science, Springer-Verlag, pp 855–874Google Scholar
  20. 20.
    Ossami D-D, Jacquot J-P, Souquières J (2005) Consistency in UML and B multi-view specifications. In: Integrated formal methods, 5th international conference, IFM 2005, vol 3771. Lecture notes in computer science, Springer-Verlag, pp 386–405Google Scholar
  21. 21.
    Satpathy M, Harrison R, Snook C, Butler M (2001) A comparative study of formal and informal specifications through an industrial case study. In: Proceedings of FSCBS′01: IEEE/IFIP Workshop on Formal Specification of Computer Based Systems. Washington, DC, pp 133–137Google Scholar
  22. 22.
    Sekerinski E (1998) Graphical design of reactive systems. In: B′98: The 2nd international B Conference, Recent advances in the development and use of the B method, vol 1393. Lecture Notes in Computer Science, Springer-Verlag, pp 182–197Google Scholar
  23. 23.
    Snook C, Butler M (2001) Using a graphical design tool for formal specification. In: Kadoba K (ed) Proceedings of the 13th annual workshop of the psychology of programming interest group, pp 311–321Google Scholar
  24. 24.
    Spivey JM (1992) The Z notation—A reference manual, 2nd edn, Prentice HallGoogle Scholar
  25. 25.
    Tatibouet B, Hammad A, Voisinet JC (2002) From an abstract B specification to UML class diagrams. In: 2nd IEEE International Symposium on Signal Processing and Information Technology (ISSPIT′2002), Marrakech, MoroccoGoogle Scholar
  26. 26.
    Tatibouet B, Voisinet JC (2003) Generating statecharts from B specifications. In: 16th International Conference on Software and Systems Engineering and Their Applications (ICSSEA′2003), CNAM—Paris, FranceGoogle Scholar
  27. 27.
    Warmer J, Kleppe A (1999) The object constraint langage: Precise modeling with UML. Addison Wesley, Reading, MAGoogle Scholar

Copyright information

© Springer Science+Business Media, LLC 2006

Authors and Affiliations

  1. 1.Laboratoire LogicielsSystèmes, Réseaux - IMAG Université Joseph FourierGrenobleFrance

Personalised recommendations