A Translation of UML Components into Formal Specifications

  • Liang Peng
  • Annya Romanczuk
  • Jean-Claude Royer
Part of the The Kluwer International Series in Engineering and Computer Science book series (SECS, volume 732)


UML demonstrated that it is a well-suited approach to analyse and design complex systems such as industrial ones. To improve software reliability and reusability the use of formal specification is necessary but it may be difficult. There is a general lack in the formal specification of the UML concepts. This decreases the ability to develop tools and guidelines to help the specifier. Software tools are needed to assist the formal specification process, but also to prove or to verify some parts. In this paper we propose a method to formally specify concurrent and communicating components with data in UML. The principle is, first to complete the design with axioms, second to translate the diagrams into algebraic specifications of data types thanks to our translation tool. We describe the translation principles which are based on previous work around symbolic transition systems and algebraic specifications. Finally, we sketch the implementation of our translation tool using XMI files and the XML4J parser.


Unify Modelling Language Unify Modelling Language Model State Predicate Abstract Data Type Prototype Verification System 
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.
    James Rumbaugh, Ivar Jacobson, and Grady Booch. The Unified Modeling Language Reference Manual. Addison-Wesley, 1999.Google Scholar
  2. 2.
    Robert France, Andy Evans, and Kevin Lano. The UML as a formal modeling notation. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds, editors, Proceedings OOPSLA′97 Workshop on Object-oriented Behavioral Semantics, pages 75–81. Technische Universität München, TUM-I9737, 1997.Google Scholar
  3. 3.
    Andy Evans. Making UML precise. In Luis Andrade, Ana Moreira, Akash Deshpande, and Stuart Kent, editors, Proceedings of the OOPSLA′98 Workshop on Formalizing UML. Why? How?, 1998.Google Scholar
  4. 4.
    Pascal Poizat, Christine Choppy, and Jean-Claude Royer. Concurrency and Data Types: a Specification Method. An Example with LOTOS. In J. Fiadero, editor, Recent Trends in Algebraic Development Techniques, Selected Papers of the 13th Workshop on Algebraic Development Techniques, WADT′98, volume 1589 of Lecture Notes in Computer Science, pages 276–291. Springer-Verlag, 1999.Google Scholar
  5. 5.
    Jean-Claude Royer. Formal Specification and Temporal Proof Techniques for Mixed Systems. In Proceedings of the 15th IPDPS 2001 Symposium, FMPPTA, San Francisco, USA, 2001. IEEE Computer Society.Google Scholar
  6. 6.
    Christine Choppy, Pascal Poizat, and Jean-Claude Royer. Specification of mixed systems in KORRIGAN with the support of a UML-inspired graphical notation. In Heinrich Huss-mann, editor, Fundamental Approaches to Software Engineering. 4th International Conference, FASE 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2–6. 2001 Proceedings, volume 2029 of LNCS, pages 124–139. Springer, 2001.Google Scholar
  7. 7.
    Stephan Garland and John Guttag. An overview of LP, the Larch Prover. In Proc. of the 3rd International Conference on Rewriting Techniques and Applications, volume 355 of Lecture Notes in Computer Science. Springer-Verlag, 1989.Google Scholar
  8. 8.
    S. Owre, J. M. Rushby, and N. Shankar. PVS: A prototype verification system. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752. Springer-Verlag, 1992.Google Scholar
  9. 9.
    Pascal André, Annya Romanczuk, Jean-Claude Royer, and Aline Vasconcelos. An Algebraic View of UML Class Diagrams. In H. Sahraoui C. Dony, editor, Acte de la conférence LMO′2000, pages 261–276, 2000. ISBN 2-6462-0093-7.Google Scholar
  10. 10.
    Pascal André, Annya Romanczuk, Jean-Claude Royer, and Aline Vasconcelos. Checking the Consistency of UML Class Diagrams Using Larch Prover. In T. Clark, editor, Proceedings of the third Rigorous Object-Oriented Methods Workshop, BCS eWics, ISBN: 1-902505-38-7, 2000.
  11. 11.
    Michel Allemand and Jean-Claude Royer. Mixed Formal Specification with PVS. In Proceedings of the 15th IPDPS 2002 Symposium, FMPPTA. IEEE Computer Society, 2002.Google Scholar
  12. 12.
    Jean-Claude Royer. Temporal Logic Verifications for UML: the Vending Machine Example. In Proceedings of the fourth Rigorous Object-Oriented Methods Workshop, 2002.Google Scholar
  13. 13.
    Kevin Lano and Juan Bicarregui. Semantics and transformations for UML models. In Pierre-Alain Muller and Jean Bézivin, editors, Proceedings of UML′98 International Workshop, Mulhouse, France, June 3–4, 1998, pages 97–106. ESSAIM, Mulhouse, France, 1998.Google Scholar
  14. 14.
    Bertrand Meyer. Object-Oriented Software Construction, 2nd Ed. Prentice-Hall, Englewood Cliffs, NJ 07632, USA, second edition, 1997.zbMATHGoogle Scholar
  15. 15.
    E. Astesiano, B.Krieg-Bruckner, and H.-J. Kreowski Eds., editors. Algebraic Foundations of System Specification. IFIP State-of-the-Art Reports. Springer Verlag, 1999. ISBN 3-540-63772-9.Google Scholar
  16. 16.
    Martin Wirsing. Algebraic Specification, volume B of Handbook of Theoretical Computer Science, chapter 13, pages 675–788. Elsevier, 1990. J. Van Leeuwen, Editor.Google Scholar
  17. 17.
    André Arnold. Finite Transition Systems. International Series in Computer Science. Prentice-Hall, 1994. ISBN 0-13-092990-5.Google Scholar
  18. 18.
    Gianna Reggio, Egidio Astesiano, Christine Choppy, and Heinrich Hussmann. Analysing UML active classes and associated state machines — A lightweight formal approach. In Tom Maibaum, editor, Proc. Fundamental Approaches to Software Engineering (FASE 2000), Berlin, Germany, volume 1783 of LNCS. Springer, 2000.Google Scholar
  19. 19.
    A. Hamie, J. Howse, and S. Kent. Interpreting the Object Constraint Language. In Proceedings of Asia Pacific Conference in Software Engineering. IEEE Press, January 1998.Google Scholar
  20. 20.
    Jean-Claude Royer. An Operational Approach to the Semantics of Classes: Application to Type Checking. Programming and Computer Software, 27(3), 2002. ISSN 0361–7688.Google Scholar
  21. 21.
    Bogumila Hnatkowska and Huzar Zbigniew. Extending the UML with a Multicast Synchronisation. In T. Clark, editor, ROOM′2000: third workshop on Rigorous Object-Oriented Methods, BCS eWics, ISBN: 1-902505-38-7, 2000. http: //
  22. 22.
    R. Clark and A. Moreira. Use of E-LOTOS in adding formality to UML. Journal of Universal Computer Science, 6(11): 1071–1087, 2000.zbMATHGoogle Scholar
  23. 23.
    Michael J. McLaughlin and Alan Moore. Real-time extensions to UML. Dr. Dobb’s Journal of Software Tools, 23(12):82, 84, 86–93, December 1998.Google Scholar
  24. 24.
    Christine Choppy, Pascal Poizat, and Jean-Claude Royer. The Korrigan Environment. Journal of Universal Computer Science, 7(1): 19–36, 2001. Special issue: Tools for System Design and Verification, ISSN: 0948–6968.zbMATHGoogle Scholar
  25. 25.
    Unisys Corp. et al. XML Metadata Interchange (XMI), October 1998. Scholar
  26. 26.
    IBM. XML4J. Technical report, 1998.
  27. 27.
    José Meseguer. Solving the inheritance anomaly in concurrent object-oriented programming. In Oscar Nierstrasz, editor, Proceedings ECOOP′93, LNCS 707, pages 220–246, Kaiserslautern, Germany, July 1993. Springer-Verlag.Google Scholar
  28. 28.
    A. M. D. Moreira and R. G. Clark. Combining Object-Oriented Analysis and Formal Description Techniques. In M. Tokoro and R. Pareschi, editors, Proceedings of ECOOP′94, Bologna, Italy, Lecture Notes in Computer Science 821, pages 344–364. Springer-Verlag, Berlin, 1994.Google Scholar
  29. 29.
    Robert G. Clark and Ana M. D. Moreira. Formal Specifications of User Requirements. Automated Software Engineering: An International Journal, 6(3):217–232, July 1999.CrossRefGoogle Scholar
  30. 30.
    A. Hamie, J. Howse, and S. Kent. Modular Semantics for Object-Oriented Models. In Proceedings of Northern Formal Methods Workshop, eWics Series. Springer Verlag, August 1998.Google Scholar
  31. 31.
    Bran Selic and Jim Rumbaugh. Using UML for Modeling Complex Real-Time Systems. Technical report, Rational Software Corp., 1998.Google Scholar

Copyright information

© Springer Science+Business Media New York 2003

Authors and Affiliations

  • Liang Peng
    • 1
  • Annya Romanczuk
    • 1
  • Jean-Claude Royer
    • 2
  1. 1.Groupe Objets, Composants, ModèlesEcole des Mines de NantesNantes Cedex 3France
  2. 2.Equipe Génie Logiciel, Méthodes et Spécifications FormellesIRIN - Université de NantesNantes Cedex 03France

Personalised recommendations