Abstract
Verifying whether a UML class diagram annotated with Object Constraint Language (OCL) constraints is consistent involves finding valid instances that provably meet its structural and OCL constraints. Recently, many tools and techniques have been proposed to find valid instances. However, they often do not scale well when the number of OCL constraints significantly increases. In this paper, we present a new tool called QMaxUSE that is capable of automatically verifying a large number of OCL invariants. QMaxUSE works by decomposing them into a set of different queries. It then uses an SMT solver to concurrently verify each query and pinpoints conflicting OCL invariants. Our evaluation results suggest that QMaxUSE can offer up to 30x efficiency improvement in verifying UML class diagrams with a large number of OCL invariants.
Chapter PDF
Similar content being viewed by others
References
Berardi, D., Calvanese, D., Giacomo, G.D.: Reasoning on UML class diagrams is EXPTIME-hard. In: International Workshop on Description Logics. (2003)
Berardi, D., Calvanese, D., Giacomo, G.D.: Reasoning on UML class diagrams. Artificial Intelligence 168(1–2) (2005) 70–118
Queralt, A., Teniente, E.: Reasoning on uml class diagrams with ocl constraints. In: Conceptual Modeling, Springer (2006) 497–512
Queralt, A., Artale, A., Calvanese, D., Teniente, E.: OCL-Lite: Finite reasoning on UML/OCL conceptual schemas. Data & Knowledge Engineering 73 (2012) 1–22
Dania, C., Clavel, M.: Ocl2msfol: A mapping to many-sorted first-order logic for efficiently checking the satisfiability of ocl constraints. In: International Conference on Model Driven Engineering Languages and Systems, ACM (2016) 65–75
Maraee, A., Balaban, M.: Efficient reasoning about finite satisfiability of UML class diagrams with constrained generalization sets. In: 3rd European Conference Model Driven Architecture, Springer (2007) 17–31
Balaban, M., Maraee, A.: Finite Satisfiability of UML Class Diagrams with Constrained Class Hierarchy. ACM Transactions on Software Engineering and Methodology 22(3) (2013) 24:1–24:42
Wu, H., Farrell, M.: A formal approach to finding inconsistencies in a metamodel. Software and Systems Modeling (2021)
González Pérez, C.A., Buettner, F., Clarisó, R., Cabot, J.: EMFtoCSP: A tool for the lightweight verification of EMF models. In: International Workshop on Formal Methods in Software Engineering: Rigorous and Agile Approaches, IEEE (2012) 44–50
Kuhlmann, M., Gogolla, M.: From uml and ocl to relational logic and back. In: International Conference on Model Driven Engineering Languages and Systems, Springer (2012) 415–431
Queralt, A., Artale, A., Calvanese, D., Teniente, E.: Ocl-lite: Finite reasoning on UML/OCL conceptual schemas. Data & Knowledge Engineering 73 (2012) 1 – 22
Wu, H.: Maxuse: A tool for finding achievable constraints and conflicts for inconsistent UML class diagrams. In: Integrated Formal Methods, Springer (2017) 348–356
Wille, R., Soeken, M., Drechsler, R.: Debugging of inconsistent UML/OCL models. In: Design, Automation Test in Europe, IEEE (2012) 1078–1083
Wu, H., Monahan, R., Power, J.F.: Exploiting attributed type graphs to generate metamodel instances using an SMT solver. In: International Symposium on Theoretical Aspects of Software Engineering, IEEE (2013) 175–182
Wu, H.: Generating metamodel instances satisfying coverage criteria via SMT solving. In: International Conference on Model-Driven Engineering and Software Development, IEEE (2016) 40–51
Soeken, M., Wille, R., Drechsler, R.: Verifying dynamic aspects of uml models. In: Design, Automation Test in Europe, IEEE (March 2011) 1–6
Wu, H.: A query-based approach for verifying UML class diagrams with OCL invariants (to appear). In: 18th European Conference on Modelling Foundations and Applications
Ehrig, K., Küster, J.M., Taentzer, G.: Generating instance models from meta models. Software and Systems Modeling 8(4) (2009) 479–500
Hoffmann, B., Minas, M.: Defining models - meta models versus graph grammars. Electronic Communications of the EASST 29 (2010) 1–14
Hoffmann, B., Minas, M.: Generating instance graphs from class diagrams with adaptive star grammars. In: International Workshop on Graph Computation Models, Electronic Communications of the EASST (2011)
Maraee, A., Balaban, M.: Removing redundancies and deducing equivalences in UML class diagrams. In: International Conference Model-Driven Engineering Languages and Systems, Springer (2014) 235–251
Semeráth, O., Nagy, A.S., Varró, D.: A graph solver for the automated generation of consistent domain-specific models. In: Proceedings of the 40th International Conference on Software Engineering. ICSE ’18, Association for Computing Machinery (2018) 969–980
Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: A challenging model transformation. In: International Conference on Model Driven Engineering Languages and Systems, Springer (2007) 436–450
Semeráth, O., Vörös, A., Varró, D.: Iterative and incremental model generation by logic solvers. In: 19th International Conference on Fundamental Approaches to Software Engineering, Springer (2016) 87–103
Kuhlmann, M., Gogolla, M.: Strengthening SAT-based validation of UML/OCL models by representing collections as relations. In: Modelling Foundations and Applications. Volume 7349. Springer (2012) 32–48
Gogolla, M., Büttner, F., Richters, M.: USE: A UML-based specification environment for validating UML and OCL. Science of Computer Programming 69(1-3) (2007) 27–34
De Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer (2008) 337–340
Gogolla, M., Büttner, F., Cabot, J.: Initiating a benchmark for UML and OCL analysis tools. In: International Conference on Tests and Proofs, Springer (2013) 115–132
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Wu, H. (2022). QMaxUSE: A Query-based Verification Tool for UML Class Diagrams with OCL Invariants. In: Johnsen, E.B., Wimmer, M. (eds) Fundamental Approaches to Software Engineering. FASE 2022. Lecture Notes in Computer Science, vol 13241. Springer, Cham. https://doi.org/10.1007/978-3-030-99429-7_17
Download citation
DOI: https://doi.org/10.1007/978-3-030-99429-7_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99428-0
Online ISBN: 978-3-030-99429-7
eBook Packages: Computer ScienceComputer Science (R0)