Coming and Going from UML to B: A Proposal to Support Traceability in Rigorous IS Development

  • Régine Laleau
  • Fiona Polack
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2272)


CEDRIC-IIE is researching rigorous information system (IS) development. Previous work includes translation rules for deriving a B specification from object-oriented diagrams, metamodels of IS UML structural and functional concepts, and a prototype translation tool. Here we outline the traceability needs for a tool to assist in rigorous IS development, and provide meta-structures for the required links among B and IS UML concepts, in the context of existing translation rules and IS UML metamodels.


Integrity Constraint Abstract Syntax Business Rule Object Management Group Traceability Link 
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.
    J-R. Abrial. The B-Book. CUP, 1996.Google Scholar
  2. 2.
    J-R. Abrial. Event driven sequential program construction. In AFADL01: Approches Formelles dans l’Assistance au Développement des Logiciels, Nancy, France, June 2001.Google Scholar
  3. 3.
    J-R. Abrial and L. Mussat. Introducing dynamic constraints in B. In B98: Second International B Conference, Montpellier, France, volume 1393 of LNCS, pages 83–128. Springer Verlag, April 1998.Google Scholar
  4. 4.
    A. Clark, A. Evans, S. Kent, and P. Sammut. The MMFapproac h to engineering object-oriented design languages. In Workshop on Language Descriptions, Tools and Applications, LTDA2001, April 2001.Google Scholar
  5. 5.
    T. Clark and A. Evans. Foundations of the Unified Modeling Language. In Second Northern Formal Methods Workshop, volume 1241 of LNCS. Springer Verlag, 1997.Google Scholar
  6. 6.
    Rational Software Corporation. Rational Rose — Using Rational Rose 98. Rational Inc., 1998.Google Scholar
  7. 7.
    DIGILOG. Atelier B, Manuel de Référence. DIGILOG groupe STERIA, BP 16000, 13791 Aix-en-Provence Cedex 3, France, 1996.Google Scholar
  8. 8.
    D. F. D’Souza and A. C. Wills. Objects, Components and Frameworks in UML: the Catalysis Approach. Addison-Wesley, 1999.Google Scholar
  9. 9.
    P. Facon, R. Laleau, A. Mammar, and F. Polack. Formal specification of the UML metamodel for building rigorous CAiSE tools. Technical report, CEDRIC Laboratory, CNAM, September 1999.Google Scholar
  10. 10.
    P. Facon, R. Laleau, and H. P. Nguyen. Dérivation de spécifications formelles B á partir de spécifications semi-formelles de systèmes d’information. In 1st B Conference, Nantes, France, 1996.Google Scholar
  11. 11.
    P. Facon, R. Laleau, and H. P. Nguyen. FromOMT diagrams to B specifications. In M. Frappier and H. Habrias, editors, Software Speci.cation Methods. An Overview Using a Case Study, pages 57–77. Springer, 2000.Google Scholar
  12. 12.
    P. Facon, R. Laleau, H. P. Nguyen, and A. Mammar. Combining UML with the B formal method for the specification of database applications. Technical report, CEDRIC Laboratory, CNAM, September 1999.Google Scholar
  13. 13.
    R. B. France and M. M. Larrondo-Petrie. A two-dimensional view of integrated formal and informal specification techniques. In Ninth International Conference of Z Users, Limerick, Ireland, September 1995, volume 967 of LNCS, pages 434–448. Springer Verlag, 1995.Google Scholar
  14. 14.
    J-C. Freire Junior. Pouvoir d’expression de modèles orientés objet. Ingénierie des Systèmes d’Information, 4(2):219–237, 1996.MathSciNetGoogle Scholar
  15. 15.
    R. Laleau and A. Mammar. A generic process to refine a B specification into a relational database implementation. In Proceedings, ZB2000: Formal Specification and Development in Z and B, York, August-September 2000, volume 1878 of LNCS, pages 22–41. Springer Verlag, 2000.Google Scholar
  16. 16.
    R. Laleau and A. Mammar. An overview of a method and its support tool for generating B specifications from UML notations. In ASE: 15th IEEE Conference on Automated Software Engineering, Grenoble, France. IEEE Computer Society Press, September 2000.Google Scholar
  17. 17.
    R. Laleau and F. Polack. Specification of integrity-preserving operations in information systems by using a formal UML-based language. Accepted for publication, Information and Software Technology, 2001.Google Scholar
  18. 18.
    Y. Ledru. Identifying preconditions with the Z/EVES theorem prover. In ASE: 13th IEEE Conference on Automated Software Engineering. IEEE Computer Society Press, October 1998.Google Scholar
  19. 19.
    B. Meyer. Object-oriented software construction. Prentice Hall, 1997.Google Scholar
  20. 20.
    E. Meyer and J. Souquières. A systematic approach to transform OMT diagrams to a B specification. In FM99, Toulouse, France, volume 1708 and 1709 of LNCS, pages 875–895. Springer Verlag, 1999.Google Scholar
  21. 21.
    F. Monge. Formalisation du méta modèle des méthodes graphiques d’analyse et conception orientèes objet. Master’s thesis, Institut d’Informatique d’Entreprise, Conservatoire National des Arts et Métiers, Evry, September 1997.Google Scholar
  22. 22.
    H. P. Nguyen. Dérivation de spécifications formelles B à partir de spécifications semi-formelles. PhD thesis, Laboratoire CEDRIC, Conservatoire National des Arts et Mètiers, Evry, December 1998. Available from
  23. 23.
    F. Polack. Exploring the informal translations of OMT object models in B. Technical report, University of York, forthcoming, 2001.Google Scholar
  24. 24.
    F. Polack and R. Laleau. A rigorous metamodel for UML static conceptual modelling of information systems. In CAiSE2001: 13th International Conference on Advanced Information Systems Engineering, Interlaken, Switzerland, volume 2068 of LNCS. Springer Verlag, June 2001.Google Scholar
  25. 25.
    J. Rumbaugh, I. Jacobson, and G. Booch. The Unified Modeling Language Reference Guide. Addison-Wesley, 1998.Google Scholar
  26. 26.
    L. T. Semmens, R. B. France, and T. W. G. Docker. Integrated structured analysis and formal specification techniques. The Computer Journal, 35(6):600–610, 1992.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Régine Laleau
    • 1
  • Fiona Polack
    • 2
  1. 1.CEDRIC-IIE(CNAM)EvryFrance
  2. 2.Department of Computer ScienceUniversity of YorkYorkUK

Personalised recommendations