Software & Systems Modeling

, Volume 18, Issue 4, pp 2655–2678 | Cite as

\(\hbox {OCL}_\textsf {FO}\): first-order expressive OCL constraints for efficient integrity checking

  • Enrico Franconi
  • Alessandro Mosca
  • Xavier OriolEmail author
  • Guillem Rull
  • Ernest Teniente
Regular Paper


OCL is the standard language for defining constraints in UML class diagrams. Unfortunately, as we show in this paper, full OCL is so expressive that it is not possible to check general OCL constraints efficiently. In particular, we show that checking general OCL constraints is not only not polynomial, but not even semidecidable. To overcome this situation, we identify \(\hbox {OCL}_\textsf {FO}\), a fragment of OCL which is expressively equivalent to relational algebra (RA). By equivalent we mean that any \(\hbox {OCL}_\textsf {FO}\) constraint can be checked through a RA query (which guarantees that \(\hbox {OCL}_\textsf {FO}\) checking is efficient, i.e., polynomial), and any RA query encoding some constraint can be written as an \(\hbox {OCL}_\textsf {FO}\) constraint (which guarantees expressiveness of \(\hbox {OCL}_\textsf {FO}\)). In this paper we define the syntax of \(\hbox {OCL}_\textsf {FO}\), we concisely determine its semantics through set theory, and we prove its equivalence to RA. Additionally, we identify the core of this language, i.e., a minimal subset of \(\hbox {OCL}_\textsf {FO}\) equivalent to RA.


OCL Relational algebra Integrity checking 



This work has been partially supported by the Ministerio de Economía y Competitividad, under Project TIN2017-87610-R, and by the Secreteria d’Universitats i Recerca de la Generalitat de Catalunya under 2017 SGR 1749.


  1. 1.
    Chen, P.P.S.: The entity-relationship model-toward a unified view of data. ACM Trans. Database Syst. (TODS) 1(1), 9–36 (1976)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Halpin, T.: Object-role modeling (orm/niam). In: Handbook on Architectures of Information Systems, pp. 81–103. Springer, Berlin(1998)Google Scholar
  3. 3.
    Object Management Group (OMG): Unified Modeling Language (UML) Superstructure Specification, version 2.4.1. (2011) Accessed 30 July 2018
  4. 4.
    Object Management Group (OMG): Object Constraint Language (UML), version 2.4. (2014) Accessed 30 July 2018
  5. 5.
    Immerman, N.: Descriptive Complexity. Springer, Berlin (2012)zbMATHGoogle Scholar
  6. 6.
    Mandel, L., Cengarle, M.V.: On the expressive power of the object constraint language OCL. FM’99–Formal Methods. Volume 1708 of Lecture Notes in Computer Science, pp. 854–874. Springer, Berlin (1999)Google Scholar
  7. 7.
    Brucker, A.D., Clark, T., Dania, C., Georg, G., Gogolla, M., Jouault, F., Teniente, E., Wolff, B.: Panel discussion: proposals for improving ocl. In: Proceedings of the MODELS 2014 OCL Workshop (OCL 2014), vol. 1285, pp. 83–99. CEUR-WS. org (2014)Google Scholar
  8. 8.
    Berardi, D., Calvanese, D., De Giacomo, G.: Reasoning on UML class diagrams. Artif. Intell. 168(1–2), 70–118 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    : Eclipse ocl project. Accessed Aug 08, 2016
  10. 10.
    Aßmann, U., Bartho, A., Bürger, C., Cech, S., Demuth, B., Heidenreich, F., Johannes, J., Karol, S., Polowinski, J., Reimann, J., Schroeter, J., Seifert, M., Thiele, M., Wende, C., Wilke, C.: Dropsbox: the dresden open software toolbox. Softw. Syst. Model. 13(1), 133–169 (2014)CrossRefGoogle Scholar
  11. 11.
    Hamann, L., Hofrichter, O., Gogolla, M.: On integrating structure and behavior modeling with OCL. In: Model Driven Engineering Languages and Systems—15th International Conference, MODELS 2012, Innsbruck, Austria, 2012. Proceedings, pp. 235–251. (2012)Google Scholar
  12. 12.
    Brucker, A.D., Tuong, F., Wolff, B.: Featherweight ocl: a proposal for a machine-checked formal semantics for ocl 2.5. Archive of Formal Proofs (Jan 2014). Formal proof development. Accessed 30 July 2018
  13. 13.
    Marković, S., Baar, T.: An OCL Semantics Specified with QVT, pp. 661–675. Springer, Berlin (2006)Google Scholar
  14. 14.
    Oriol, X., Teniente, E.: Incremental checking of ocl constraints with aggregates through sql. In: Conceptual Modeling: 34th International Conference, ER, Cham, pp. 199–213. Springer (2015)Google Scholar
  15. 15.
    Franconi, E., Mosca, A., Oriol, X., Rull, G., Teniente, E.: Logic foundations of the ocl modelling language. In: European Workshop on Logics in Artificial Intelligence, pp. 657–664. Springer (2014)Google Scholar
  16. 16.
    Oriol, X., Teniente, E., Tort, A.: Computing repairs for constraint violations in uml/ocl conceptual schemas. Data Knowl. Eng. 99, 39–58 (2015)CrossRefGoogle Scholar
  17. 17.
    Queralt, A., Artale, A., Calvanese, D., Teniente, E.: OCL-Lite: finite reasoning on UML/OCL conceptual schemas. Data Knowl. Eng. 73, 1–22 (2012)CrossRefGoogle Scholar
  18. 18.
    Linz, P.: An Introduction to Formal Languages and Automata. Jones & Bartlett Learning, Burlington (1990)zbMATHGoogle Scholar
  19. 19.
    Queralt, A., Teniente, E.: Verification and validation of uml conceptual schemas with ocl constraints. ACM Trans. Softw. Eng. Methodol. 21(2), 13:1–13:41 (2012)Google Scholar
  20. 20.
    Planas, E., Olivé, A.: The DBLP case study (2006). Accessed 30 July 2018
  21. 21.
    Tort, A.: The osCommerce case study Accessed 30 July 2018
  22. 22.
    ANSI Standard: The SQL 92 Standard (1992)Google Scholar
  23. 23.
    Bergmann, G.: Translating OCL to graph patterns. In: Model-Driven Engineering Languages and Systems—17th International Conference, MODELS 2014, Valencia, Spain, 2014. Proceedings, pp. 670–686 (2014)Google Scholar
  24. 24.
    Egea, M., Dania, C.: Sql-pl4ocl: an automatic code generator from ocl to sql procedural language. Softw. Syst. Model. (2017).
  25. 25.
    Hilken, F., Niemann, P., Gogolla, M., Wille, R.: From UML/OCL to base models: transformation concepts for generic validation and verification. In: Theory and Practice of Model Transformations—8th International Conference, ICMT 2015, Held as Part of STAF 2015, L’Aquila, Italy, July 20–21, 2015. Proceedings, pp. 149–165 (2015)Google Scholar
  26. 26.
    Balsters, H.: Modelling database views with derived classes in the UML/OCL-framework. In: UML2003-The Unified Modeling Language. Modeling Languages and Applications, pp. 295–309. Springer (2003)Google Scholar
  27. 27.
    Queralt, A., Teniente, E.: Verification and validation of UML conceptual schemas with OCL constraints. ACM Trans. Softw. Eng. Methodol. 21(2), 13 (2012)CrossRefGoogle Scholar
  28. 28.
    Clavel, M., Egea, M., de Dios, M.A.G.: Checking unsatisfiability for OCL constraints. In: Proceedings of the Workshop the Pragmatics of OCL and Other Textual Specification Languages, vol. 24. ECEASST (2009)Google Scholar
  29. 29.
    Beckert, B., Keller, U., Schmitt, P.H.: Translating the object constraint language into first-order predicate logic. In: Proceedings of VERIFY, Workshop at Federated Logic Conferences (FLoC) (2002)Google Scholar
  30. 30.
    Egea, M., Dania, C., Clavel, M.: MySQL4OCL: a stored procedure-based MySQL code generator for OCL. Electron. Commun. EASST 36, 1–16 (2010)Google Scholar
  31. 31.
    Demuth, B., Hussmann, H.: Using UML/OCL constraints for relational database design. In: «UML»99—The Unified Modeling Language, pp. 598–613. Springer (1999)Google Scholar
  32. 32.
    Oriol, X., Teniente, E.: Ocl\({}_{\text{univ}}\): expressive UML/OCL conceptual schemas for finite reasoning. In: Mayr, H. C., Guizzardi, G., Ma, H., Pastor, O. (eds.) Conceptual Modeling—36th International Conference, ER 2017, Valencia, Spain, Nov 6–9, 2017, Proceedings, pp. 354–369 (2017)Google Scholar
  33. 33.
    Fagin, R., Kolaitis, P.G., Miller, R.J., Popa, L.: Data exchange: semantics and query answering. Theor. Comput. Sci. 336(1), 89–124 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  34. 34.
    Cunha, A., Garis, A.G., Riesco, D.: Translating between alloy specifications and UML class diagrams annotated with OCL. Softw. Syst. Model. 14(1), 5–25 (2015)CrossRefGoogle Scholar
  35. 35.
    Kuhlmann, M., Gogolla, M.: From UML and OCL to relational logic and back. In: Model Driven Engineering Languages and Systems—15th International Conference, MODELS 2012, Innsbruck, Austria, Sept 30–Oct 5, 2012. Proceedings, pp. 415–431 (2012)Google Scholar
  36. 36.
    Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: On challenges of model transformation from UML to alloy. Softw. Syst. Model. 9(1), 69–86 (2010)CrossRefGoogle Scholar
  37. 37.
    González, C.A., Büttner, F., Clarisó, R., Cabot, J.: Emftocsp: a tool for the lightweight verification of EMF models. In: Proceedings of the First International Workshop on Formal Methods in Software Engineering—Rigorous and Agile Approaches, FormSERA 2012, Zurich, Switzerland, June 2, 2012, pp. 44–50. (2012)Google Scholar
  38. 38.
    Soeken, M., Wille, R., Drechsler, R.: Encoding OCL data types for sat-based verification of UML/OCL models. In: Tests and Proofs—5th International Conference, TAP 2011, Zurich, Switzerland, June 30–July 1, 2011. Proceedings, pp. 152–170 (2011)Google Scholar
  39. 39.
    Kuhlmann, M., Gogolla, M.: Strengthening sat-based validation of UML/OCL models by representing collections as relations. In: Modelling Foundations and Applications—8th European Conference, ECMFA 2012, Kgs. Lyngby, Denmark, July 2–5, 2012. Proceedings, pp. 32–48 (2012)Google Scholar

Copyright information

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

Authors and Affiliations

  • Enrico Franconi
    • 1
  • Alessandro Mosca
    • 2
  • Xavier Oriol
    • 3
    Email author
  • Guillem Rull
    • 4
  • Ernest Teniente
    • 3
  1. 1.Free University of Bozen-BolzanoBolzanoItaly
  2. 2.SIRIS AcademicBarcelonaSpain
  3. 3.Universitat Politècnica de CatalunyaBarcelonaSpain
  4. 4.Universitat de BarcelonaBarcelonaSpain

Personalised recommendations