Skip to main content
SpringerLink
Log in
Book cover

International Conference on Integrated Formal Methods

IFM 2017: Integrated Formal Methods pp 348–356Cite as

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

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10510))

Abstract

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.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    Available at: https://github.com/classicwuhao/uran.

  2. 2.

    Note that since the rank for each constraint is equal, this means that a weighted MaxSMT can be treated as a MaxSMT problem.

References

  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

    Chapter  Google Scholar 

  2. Wille, R., Soeken, M., Drechsler, R.: Debugging of inconsistent UML/OCL models. In: 2012 DATE, pp. 1078–1083 (2012)

    Google Scholar 

  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. 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. Wu, H.: Finding achievable features and contraint conflicts for inconsistent metamodels. In: 13th ECMFA (2017, to appear)

    Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  7. Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason. 40(1), 1–33 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  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. 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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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. Clavel, M., Egea, M., de Dios, M.A.G.: Checking unsatisfiability for OCL constraints. ECEASST 24, 13 (2009)

    Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  15. Beckert, B., Hähnle, R., Schmitt, P.H.: Verification of Object-Oriented Software: The KeY Approach. Springer, Berlin, Heidelberg (2007)

    MATH  Google Scholar 

  16. Wu, H.: Generating metamodel instances satisfying coverage criteria via SMT solving. In: The 4th MODELSWARD, pp. 40–51 (2016)

    Google Scholar 

  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

    Chapter  Google Scholar 

  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. 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. Cabot, J., Clarisó, R., Riera, D.: On the verification of UML/OCL class diagrams using constraint programming. J. Syst. Softw. 93, 1–23 (2014)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, National University of Ireland, Maynooth, Maynooth, Republic of Ireland

    Hao Wu

Authors
  1. Hao Wu
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hao Wu .

Editor information

Editors and Affiliations

  1. Massachusetts Institute of Technology, Cambridge, Massachusetts, USA

    Nadia Polikarpova

  2. University of Surrey, Guildford, United Kingdom

    Steve Schneider

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Wu, H. (2017). MaxUSE: A Tool for Finding Achievable Constraints and Conflicts for Inconsistent UML Class Diagrams. In: Polikarpova, N., Schneider, S. (eds) Integrated Formal Methods. IFM 2017. Lecture Notes in Computer Science(), vol 10510. Springer, Cham. https://doi.org/10.1007/978-3-319-66845-1_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66845-1_23

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66844-4

  • Online ISBN: 978-3-319-66845-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation