Formalizing UML/OCL structural features with FoCaLiZe

  • Messaoud AbbasEmail author
  • Choukri-Bey Ben-Yelles
  • Renaud Rioboo
Methodologies and Application


Unified Modeling Language (UML) is the de facto standard for the development of software models, and Object Constraint Language (OCL) is used within UML models to specify model constraints. Several UML/OCL tools provide Model-Driven Engineering transformation into general object-oriented programming languages such as Java and C++. But the latter did not provide mechanisms for the specification and the verification of OCL constraints. In this context, formal methods are largely used for the specification of UML/OCL models and the verification of their OCL constraints. However, the divergence between UML (object-oriented modeling) and formal methods (mathematical- and logical-based tools) leads in general to ignore most UML/OCL architectural and conceptual features such as OCL constraints simple and multiple inheritance, late binding, template binding and dependencies. To address the formalization of these features, we have used FoCaLiZe, an object-oriented development environment using a proof-based formal approach. More precisely, we propose a formal transformation of the essential UML/OCL features into FoCaLiZe specifications. The derived formal model reflects perfectly the structural features of the original UML/OCL model. In addition, it is possible to check and prove model properties using Zenon, the automatic theorem prover of FoCaLiZe.


Software engineering Model-Driven Engineering Formal methods Functional programming UML modeling Semantics 


Compliance with ethical standards

Conflict of interest

The authors declare that they have no conflict of interest.

Ethical approval

This article does not contain any studies with human participants or animals performed by any of the authors.

Supplementary material


  1. Abbas M (2014) Using FoCaLiZe to check OCL constraints on UML classes. In: International conference on information technology for organization development, IT4OD 2014, conference proceedings, pp 31–38Google Scholar
  2. Abbas M, Ben-Yelles CB, Rioboo R (2014) Modeling UML template classes with FoCaLiZe. In: The international conference on integrated formal methods, IFM2014, LNCS, vol 8739. Springer, pp 87–102Google Scholar
  3. Abbas M, Ben-Yelles CB, Rioboo R (2018) Modelling UML state machines with FoCaLiZe. Int J Inf Commun Technol 13(1):34–54Google Scholar
  4. Abrial JR (2005) The B-book: assigning programs to meanings. Cambridge University Press, CambridgezbMATHGoogle Scholar
  5. Anastasakis K, Bordbar B, Georg G, Ray I (2010) On challenges of model transformation from UML to Alloy. Softw Syst Model 9(1):69–86CrossRefGoogle Scholar
  6. Ayrault P, Hardin T, Pessaux F (2009) Development life-cycle of critical software under FoCaL. Electron Notes Theor Comput Sci 243:15–31CrossRefGoogle Scholar
  7. Beckert B, Hähnle R, Schmitt P (2007) Verification of object-oriented software: the key approach, vol 4334. LNAI. Springer, Berlin, pp 1–18Google Scholar
  8. Bonichon R, Delahaye D, Doligez D (2007) Zenon: an extensible automated theorem prover producing checkable proofs. In: Logic for programming, artificial intelligence, and reasoning. Springer, pp 151–165Google Scholar
  9. Brucker A, Wolff B (2007) The HOL-OCL book. Swiss Federal Institute of Technolgy (ETH). Accessed 3 Dec 2019
  10. Cabot J, Clarisó R, Riera D (2007) Umltocsp: a tool for the formal verification of UML/OCL models using constraint programming. In: Proceedings of the twenty-second IEEE/ACM international conference on automated software engineering. ACM, pp 547–548Google Scholar
  11. Carreira PJ, Costa ME (2003) Automatically verifying an object-oriented specification of the steam-boiler system. Sci Comput Program 46(3):197–217CrossRefzbMATHGoogle Scholar
  12. Chama W, Chaoui A, Rehab S (2015) Formal modeling and analysis of object oriented systems using triple graph grammars. Int J Embed Real-Time Commun Syst (IJERTCS) 6(2):48–64CrossRefGoogle Scholar
  13. Clavel M, Egea M (2006) ITP/OCL: a rewriting-based validation tool for UML+ OCL static class diagrams. In: 11th international conference on algebraic methodology and software technology. LNCS, vol 4019. Springer, pp 368–373Google Scholar
  14. Clavel M, Durán F, Eker S, Lincoln P, Martí-Oliet N, Meseguer J, Talcott C (2007) All about Maude a high performance logical framework: how to specify, program and verify systems in rewriting logic. Springer, BerlinzbMATHGoogle Scholar
  15. Coq (2016) The Coq Proof Assistant, tutorial and reference manual, version 8.5. INRIA–LIP–LRI–LIX–PPS. Accessed 3 Dec 2019
  16. Cunha A, Garis A, Riesco D (2013) Translating between Alloy specifications and UML class diagrams annotated with OCL constraints. Softw Syst Model 14(1):5–25CrossRefGoogle Scholar
  17. Cunha A, Garis A, Riesco D (2015) Translating between Alloy specifications and UML class diagrams annotated with OCL. Softw Syst Model 14(1):5–25CrossRefGoogle Scholar
  18. Delahaye D, Étienne J, Donzeau-Gouge V (2008a) Producing UML models from Focal specifications: an application to Airport Security Regulations. In: 2nd IFIP/IEEE international symposium on theoretical aspects of software engineering, pp 121–124Google Scholar
  19. Delahaye D, Étienne JF, Donzeau-Gouge VV (2008b) A formal and sound transformation from Focal to UML: an application to airport security regulations. Innov Syst Softw Eng 4(3):267–274CrossRefGoogle Scholar
  20. Doligez D (2016) The Zenon Tool. Software and Documentations freely available at Accessed 3 Dec 2019
  21. Durán F, Gogolla M, Roldán M (2011) Tracing properties of UML and OCL models with Maude. arXiv preprint arXiv:1107.0068 [csSE]
  22. Favre LM (2010) Formalization of MOF-based metamodels. In: Model driven architecture for reverse engineering technologies: strategic directions and system evolution, IGI Global, pp 49 –79 Google Scholar
  23. Fechter S (2005) Sémantique des traits orientés objet de FoCaL. Ph.D. thesis, Université PARIS 6Google Scholar
  24. Hardin T, Francois P, Pierre W, Damien D (2016) FoCaLiZe : tutorial and reference manual, version 0.9.1. CNAM-INRIA-LIP6. Accessed 3 Dec 2019
  25. Jackson D (2012) Software Abstractions: logic, language, and analysis. MIT Press, CambridgeGoogle Scholar
  26. Ke W, Li X, Liu Z, Stolz V (2012) rCOS: a formal model-driven engineering method for component-based software. Front Comput Sci 6(1):17–39MathSciNetzbMATHGoogle Scholar
  27. Kwon G (2000) Rewrite rules and operational semantics for model checking UML statecharts. In: UML2000—the Unified Modeling Language. LNCS, vol 1939. Springer, pp 528–540Google Scholar
  28. Ledang H, Souquières J, Charles S et al (2003) Argouml+ B: Un Outil de Transformation Systématique de Spécifications UML en B. In: AFADL’2003, pp 3–18Google Scholar
  29. Lilius J, Paltor IP (1999) vUML: a tool for verifying UML models. In: 14th IEEE international conference on automated software engineering, pp 255–258Google Scholar
  30. Miller J, Mukerji J et al (2003) MDA guide. Object Management Group, Inc, version 101Google Scholar
  31. Mosses P (2004) CASL reference manual: the complete documentation of the common algebraic specification language, vol 2960. LNCS. Springer, BerlinCrossRefzbMATHGoogle Scholar
  32. Nimiya A, Yokigawa T, Miyazaki H, Amasaki S, Sato Y, Hayase M (2010) Model checking consistency of UML diagrams using Alloy. World Acad Sci Eng Technol 71(99):547–550Google Scholar
  33. Nipkow T, Paulson LC, Wenzel M (2002) Isabelle/HOL: a proof assistant for higher-order logic, vol 2283. LNCS. Springer, BerlinCrossRefzbMATHGoogle Scholar
  34. OMG (2014) OCL: object constraint language 2.4. Accessed 3 Dec 2019
  35. OMG (2015) UML: Unified Modeling Language, version 2.5. Accessed 3 Dec 2019
  36. Reggio G, Cerioli M, Astesiano E (2001) Towards a rigorous semantics of UML supporting its multiview approach. In: Fundamental approaches to software engineering. LNCS 2029. Springer, Berlin, pp 171–186Google Scholar
  37. Rull G, Farré C, Queralt A, Teniente E, Urpí T (2015) AuRUS: explaining the validation of UML/OCL conceptual schemas. Softw Syst Model 14(2):953–980CrossRefGoogle Scholar
  38. Said MY, Butler M, Snook C (2015) A method of refinement in UML-B. Softw Syst Model 14(4):1557–1580CrossRefGoogle Scholar
  39. Snook C, Butler M (2006a) U2B - a tool for translating UML-B models into B. ACA Trans Softw Eng Methodol 15:92–122.
  40. Snook C, Butler M (2006b) UML-B: formal modeling and design aided by UML. ACM Trans Softw Eng Methodol 15:92–122CrossRefGoogle Scholar
  41. Tao L, Fengsheng J (2015) B formal modeling based on UML class. In: IEEE international conference on signal processing, communications and computing (ICSPCC), 2015. IEEE Conference Publications, pp 1–6.
  42. Truong N, Souquières J (2006) Verification of UML model elements using B. J Inf Sci Eng 22:357–373 Google Scholar
  43. W3C (2014) XSL transformations (XSLT) version 3.0, W3C recommendation, Oct 2014. Accessed 3 Dec 2019
  44. Yang J (2009) A framework for formalizing UML models with formal language rCOS. In: Fourth international conference on frontier of computer science and technology, 2009 (FCST’09). IEEE, pp 408–416Google Scholar

Copyright information

© Springer-Verlag GmbH Germany, part of Springer Nature 2019

Authors and Affiliations

  • Messaoud Abbas
    • 1
    Email author
  • Choukri-Bey Ben-Yelles
    • 2
  • Renaud Rioboo
    • 3
  1. 1.LABTHOP, College of Exacts SciencesEl Oued UniversityEl OuedAlgeria
  2. 2.LCISUniv. Grenoble AlpesValenceFrance
  3. 3.SAMOVARENSIIEEvryFrance

Personalised recommendations