Model Driven Engineering (MDE) [1] promotes models as cornerstone components in software development. Verification and validation of models become important activities to ensure the quality of a system. Effective model verification and validation methods can reduce time to market and decrease development costs. In the context of MDE, the Unified Modeling Language (UML) and the Object Constraint Language (OCL) constitute two of the most commonly used modeling languages. UML [2] has been widely accepted as the de-facto standard object-oriented software modeling language. OCL [3] is an integral part of UML which has been introduced into UML as a declarative language to express integrity constraints that UML diagrams cannot convey by themselves.

Software models, as any other software artifact, may contain defects. Unfortunately, in some occasions, possible design flaws are not detected until the later implementation stages, thus increasing the cost of development [4, 5]. This situation requires a wide adoption of formal methods as well as verification and validation approaches. In this line, there have been remarkable efforts to formalize UML semantics, and to address and solve ambiguity, uncertainty, and underspecification issues detected in UML semantics. In particular, the formalization and analysis of specific UML artifacts can be done by carrying out a translation to another language that preserves the semantics [4, 5, 6, 7, 8, 9]. The resulting translation can be used for several purposes, such as to reason about implicit properties in UML models and about particular model instances.

In this paper, Béatriz Pérez and Ivan Porres propose an overall framework to reason about specific UML Class Diagram (CDs) based on the Constraint Logic programming (CLP) paradigm. More specifically, we focus on UML Class Diagrams, annotated with OCL constraints, which are considered to be the mainstay of object-oriented analysis and design representing the static structure of a system, and whose formalization and analysis have motivated a significant number of proposals [4, 10, 11]. As reasoning tool, we use a model–finding and design space exploration tool called Formula [12], which presents distinctive strength properties compared to other similar tools, including more expressivity [13, 14]. More specifically, Formula is based on algebraic data types and CLP, and relies on the Formula solver Z3 as underlying engine to reason about models where proof goals are encoded as CLP satisfiability problem. Formula utilizes a bounded verification approach by means of which the reasoning process is carried out by establishing finite bounds for the number of instances of the model to be considered during the verification process. In the case that Z3 finds a solution that satisfies all encoded constraints, Formula will reconstruct a complete model from this information derived of known facts.

The overall framework we propose to reason about class diagram models annotated with OCL constraints consists of two steps:

  1.  translating the class diagram model to the Formula language and,
  2. using Formula for reasoning about such a model. The overview of our framework is represented diagrammatically below.


The main contribution of our work is the translation of a UML model into a Constraint Satisfaction Problem following a multilevel Meta–Object Facility (MOF) like framework. Model reasoning can be automated using the model–finding tool Formula. We have also identified a fragment of OCL, which can be checked for finite satisfiability, while being considerably expressive. We also show how to translate such an OCL fragment to Formula by giving, as an intermediate step, a representation of the OCL constraints as FOL expressions. An example is provided below.

Our approach has several direct applications. It can be used to rigorously reason about a UML design, by checking predefined correctness properties about the original model, such as satisfiability or the lack of redundant constraints [5]. Additionally, our proposal can be used to inspect models of complex system development contexts, to search for conforming object models and to choose those that better fit domain needs. Overall, our proposal can contribute to improve the software design validation and verification process.


[1]      J. Bézivin, Model driven engineering: an emerging technical space, in: Proceedings of GTTSE 05, Springer-Verlag, Berlin, 2006, pp. 36–64.

[2]      OMG, UML 2.4.1 Superstructure Specification, august, 2012. Available at: Last visited on July 2018.

[3]      OCL, Version 2.3.1, Last visited on July 2018.

[4]      A. Calí, D. Calvanese, G. D. Giacomo, M. Lenzerini, A Formal Framework for Reasoning on UML Class Diagrams, in: Proceedings of ISMIS 02, Springer, 2002, pp. 503–513.

[5]      J. Cabot, R. Clarisó, D. Riera, Verification of UML/OCL Class Diagrams using Constraint Programming, in: Proceedings of ICSTW 08, IEEE Computer Society, 2008, pp. 73–80.

[6]      B. Beckert, U. Keller, P. H. Schmitt, Translating the Object Constraint Language into First-order Predicate Logic, in: Proceedings of FLoC 02, 2002, pp. 113–123.

[7]      S. Maoz, J. O. Ringert, B. Rumpe, CD2Alloy: Class Diagrams Analysis Using Alloy Revisited., in: Proceedings of MoDELS 11, 2011, pp. 592–607.

[8]      J. M. Bruel, R. B. France, Transforming UML Models to Formal Specifications, in: Proceedings of OOPSLA 98, Springer, 1998, pp. 78–92.

[9]      W. E. McUmber, B. H. C. Cheng, A general framework for formalizing UML with formal languages, in: Proceedings of ICSE 01, IEEE Computer Society, 2001, pp. 433–442.

[10]  M. Broy, M. V. Cengarle, H. Gr¨onniger, B. Rumpe, Considerations and Rationale for a UML System Model, in: K. Lano (Ed.), UML 2 Semantics and Applications, John Wiley & Sons, Hoboken, 2009, pp. 43–60.

[11]  J. Osis, U. Donins, Formalization of the UML Class Diagrams, in: Evaluation of Novel Approaches to Software Engineering, Vol. 69 of Communications in Computer and Information Science, Springer, 2010, pp. 180–192.

[12]  FORMULA – Modeling Foundations, Last visited on July 2018.

[13]  E. K. Jackson, E. Kang, M. Dahlweid, D. Seifert, T. Santen, Components, platforms and possibilities: towards generic automation for MDA, in: Proceedings of EMSOFT 10), ACM, 2010, pp. 39–48.

[14]  E. K. Jackson, T. Levendovszky, D. Balasubramanian, Reasoning about Metamodeling with Formal Specifications and Automatic Proofs, in: Proceedings of MODELS 11, Springer, 2011, pp. 653–667.

Share This