MaxUSE: A Tool for Finding Achievable Constraints and Conflicts for Inconsistent UML Class Diagrams

Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)


In the context of Model Driven Engineering (MDE), the structure of a system is typically described by using a UML class diagram annotated with a set of Object Constraint Language (OCL) constraints. These constraints specify rules that are not expressible by using structural features. These constraints can be conflicting, resulting in inconsistencies. When this happens, the existing tools terminate and provide no information about which constraints are achievable and which ones cause conflicts. In this paper, we present MaxUSE, a tool for finding achievable OCL constraints and conflicts for inconsistent UML class diagrams. MaxUSE integrates the USE modeling tool with a satisfiability modulo theories (SMT) solver. It finds a set of achievable constraints based on their rankings by casting to a weighted MaxSMT problem and at the same time locates constraint conflicts. We use an example to demonstrate MaxUSE’s usage scenarios and discuss its usefulness to the community.


  1. 1.
    Kuhlmann, M., Hamann, L., Gogolla, M.: Extensive validation of OCL models by integrating SAT solving into USE. In: Bishop, J., Vallecillo, A. (eds.) TOOLS 2011. LNCS, vol. 6705, pp. 290–306. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-21952-8_21 CrossRefGoogle Scholar
  2. 2.
    Wille, R., Soeken, M., Drechsler, R.: Debugging of inconsistent UML/OCL models. In: 2012 DATE, pp. 1078–1083 (2012)Google Scholar
  3. 3.
    Wu, H., Monahan, R., Power, J.F.: Exploiting attributed type graphs to generate metamodel instances using an SMT solver. In: 7th TASE. Birmingham, UK (2013)Google Scholar
  4. 4.
    Dania, C., Clavel, M.: Ocl2msfol: A mapping to many-sorted first-order logic for efficiently checking the satisfiability of OCL constraints. In: 19th MoDELS, pp. 65–75. ACM (2016)Google Scholar
  5. 5.
    Wu, H.: Finding achievable features and contraint conflicts for inconsistent metamodels. In: 13th ECMFA (2017, to appear)Google Scholar
  6. 6.
    Gogolla, M., Büttner, F., Richters, M.: USE: A UML-based specification environment for validating UML and OCL. Sci. Comput. Program. 69(1–3), 27–34 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. 40(1), 1–33 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Beckert, B., Keller, U., Schmitt, P.H.: Translating the object constraint language into first-order predicate logic. In: FLoC @ 3rd Federated Logic Conferences, Denmark (2002)Google Scholar
  9. 9.
    Maraee, A., Balaban, M.: Efficient reasoning about finite satisfiability of UML class diagrams with constrained generalization sets. In: Akehurst, D.H., Vogel, R., Paige, R.F. (eds.) ECMDA-FA 2007. LNCS, vol. 4530, pp. 17–31. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-72901-3_2 CrossRefGoogle Scholar
  10. 10.
    Soeken, M., Wille, R., Drechsler, R.: Encoding OCL data types for SAT-based verification of UML/OCL models. In: Gogolla, M., Wolff, B. (eds.) TAP 2011. LNCS, vol. 6706, pp. 152–170. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-21768-5_12 CrossRefGoogle Scholar
  11. 11.
    Büttner, F., Egea, M., Cabot, J.: On verifying ATL transformations using ‘off-the-shelf’ SMT solvers. In: 15th MoDELS, pp. 432–448 (2012)Google Scholar
  12. 12.
    Clavel, M., Egea, M., de Dios, M.A.G.: Checking unsatisfiability for OCL constraints. ECEASST 24, 13 (2009)Google Scholar
  13. 13.
    Brucker, A.D., Wolff, B.: HOL-OCL: A formal proof environment for uml/ocl. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 97–100. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-78743-3_8 CrossRefGoogle Scholar
  14. 14.
    Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: A challenging model transformation. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol. 4735, pp. 436–450. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-75209-7_30 CrossRefGoogle Scholar
  15. 15.
    Beckert, B., Hähnle, R., Schmitt, P.H.: Verification of Object-Oriented Software: The KeY Approach. Springer, Berlin, Heidelberg (2007)zbMATHGoogle Scholar
  16. 16.
    Wu, H.: Generating metamodel instances satisfying coverage criteria via SMT solving. In: The 4th MODELSWARD, pp. 40–51 (2016)Google Scholar
  17. 17.
    Torlak, E., Jackson, D.: Kodkod: A relational model finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-71209-1_49 CrossRefGoogle Scholar
  18. 18.
    González Pérez, C.A., Buettner, F., Clarisó, R., Cabot, J.: EMFtoCSP: A tool for the lightweight verification of EMF models. In: SEMF: Rigorous and Agile Approaches, Zurich, Suisse (2012)Google Scholar
  19. 19.
    Cabot, J., Clarisó, R., Riera, D.: Verification of UML/OCL class diagrams using constraint programming. In: IEEE STV&V Workshop, pp. 73–80. IEEE Computer Society, Berlin, Germany (2008)Google Scholar
  20. 20.
    Cabot, J., Clarisó, R., Riera, D.: On the verification of UML/OCL class diagrams using constraint programming. J. Syst. Softw. 93, 1–23 (2014)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Department of Computer ScienceNational University of Ireland, MaynoothMaynoothRepublic of Ireland

Personalised recommendations