{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,22]],"date-time":"2026-06-22T04:47:05Z","timestamp":1782103625773,"version":"3.54.5"},"reference-count":52,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2026,5,25]],"date-time":"2026-05-25T00:00:00Z","timestamp":1779667200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,5,25]],"date-time":"2026-05-25T00:00:00Z","timestamp":1779667200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["250902306"],"award-info":[{"award-number":["250902306"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Innovations Syst Softw Eng"],"published-print":{"date-parts":[[2026,6]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Models are the primary source-artifacts in model-driven development and are thus subject to changes and evolution throughout the development process. To better understand these model-changes, semantic differencing operators can be employed. In this paper, we present an approach for automatically detecting the semantic differences of class diagrams (CDs) that have been extended with object constraint language (OCL) constraints. Previous works regarding OCL models focused mostly on validation and satisfiability of OCL invariants and conditions, not analyzing semantic differences between subsequent versions of CDs and OCL models. While implementations of semantic differencing operators for CDs already exist, they have yet to integrate OCL models in their analysis. Using a translation of CDs and OCL constraints to SMT, we developed a tool for detecting semantic differences between two compositions of CD and OCL models. The differences are reported in the form of object diagrams (ODs) that describe valid instances of one model but not the other, and the refinement of invariants is traced across models. In addition to invariants, we also consider semantic differencing of operation constraints in OCL, as well as the supplementary translation of ODs to SMT for further restricting or completing instances. The implementation of this tool is publicly available.<\/jats:p>","DOI":"10.1007\/s11334-026-00630-y","type":"journal-article","created":{"date-parts":[[2026,5,25]],"date-time":"2026-05-25T04:20:53Z","timestamp":1779682853000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Semantic difference analysis for model compositions of class diagrams, OCL constraints, and object diagrams"],"prefix":"10.1007","volume":"22","author":[{"given":"Bernhard","family":"Rumpe","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Max","family":"Stachon","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sebastian","family":"St\u00fcber","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Valdes","family":"Voufo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,5,25]]},"reference":[{"key":"630_CR1","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1080\/07421222.2004.11045786","volume":"20","author":"AM Hickey","year":"2004","unstructured":"Hickey AM, Davis AM (2004) A unified model of requirements elicitation. J Manag Inf Syst 20:65\u201384. https:\/\/doi.org\/10.1080\/07421222.2004.11045786","journal-title":"J Manag Inf Syst"},{"key":"630_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-58862-9","volume-title":"Agile modeling with UML: code generation","author":"B Rumpe","year":"2017","unstructured":"Rumpe B (2017) Agile modeling with UML: code generation. Testing, Refactoring (Springer International"},{"key":"630_CR3","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1016\/j.infsof.2018.06.010","volume":"103","author":"E Sunitha","year":"2018","unstructured":"Sunitha E, Samuel P (2018) Object constraint language for code generation from activity models. Inf Softw Technol 103:92\u2013111","journal-title":"Inf Softw Technol"},{"key":"630_CR4","doi-asserted-by":"crossref","unstructured":"Maoz S, Ringert JO, Rumpe B (2010) A Manifesto for Semantic Model Differencing. Proceedings Int. Workshop on Models and Evolution (ME\u201910), LNCS 6627, Springer, pp 194\u2013203","DOI":"10.1007\/978-3-642-21210-9_19"},{"issue":"2","key":"630_CR5","first-page":"1","volume":"22","author":"JO Ringert","year":"2023","unstructured":"Ringert JO, Rumpe B, Stachon M (2023) On implementing open world semantic differencing for class diagrams. J Object Technol (JOT) 22(2):1\u201314","journal-title":"J Object Technol (JOT)"},{"key":"630_CR6","unstructured":"Group OM (2017) Omg unified modeling language (omg uml)"},{"key":"630_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33933-7","volume-title":"Modeling with UML: language","author":"B Rumpe","year":"2016","unstructured":"Rumpe B (2016) Modeling with UML: language. Concepts, Methods (Springer International"},{"key":"630_CR8","unstructured":"Barrett C, Stump A, Tinelli C et\u00a0al (2010) The smt-lib standard: version 2.0. Proceedings of the 8th international workshop on satisfiability modulo theories Vol 13, Edinburgh, UK, pp 14"},{"key":"630_CR9","doi-asserted-by":"crossref","unstructured":"De\u00a0Moura L, Bj\u00f8rner N (2008) Z3: an efficient smt solver. International conference on tools and algorithms for the construction and analysis of systems, Springer, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"630_CR10","doi-asserted-by":"crossref","unstructured":"Rumpe B, Stachon M, St\u00fcber S, Voufo V (2024) Semantic difference analysis with invariant tracing for class diagrams extended by OCL. Workshop on Model Driven Engineering, Verification and Validation (MoDeVVa), MODELS Companion \u201924, ACM, pp 1066\u20131075","DOI":"10.1145\/3652620.3687818"},{"key":"630_CR11","doi-asserted-by":"crossref","unstructured":"Kent S, Evans A, Rumpe B, Moreira A, Demeyer S (1999) UML Semantics FAQ. In: Moreira A, Demeyer S (eds) Object-Oriented Technology, ECOOP\u201999 Workshop Reader, LNCS 1743 Springer Verlag, Berlin","DOI":"10.1007\/3-540-46589-8_3"},{"key":"630_CR12","doi-asserted-by":"crossref","unstructured":"Richters M, Gogolla M, Evans A, Kent S, Selic B (2000) Validating uml models and ocl constraints. In: Evans A, Kent S, Selic B (eds) UML 2000 \u2014 The Unified Modeling Language, Springer, Berlin, Heidelberg, pp 265\u2013277","DOI":"10.1007\/3-540-40011-7_19"},{"key":"630_CR13","doi-asserted-by":"crossref","unstructured":"Richters M, Gogolla M, Ling T-W, Ram S, Li\u00a0Lee M (1998) On formalizing the uml object constraint language ocl. In: Ling T-W, Ram S, Li\u00a0Lee M (eds) Conceptual Modeling \u2013 ER \u201998, Springer, Heidelberg, Berlin, pp 449\u2013464","DOI":"10.1007\/978-3-540-49524-6_35"},{"key":"630_CR14","doi-asserted-by":"crossref","unstructured":"Soeken M, Wille R, Kuhlmann M, Gogolla M, Drechsler R (2010) Verifying uml\/ocl models using boolean satisfiability. 2010 Design, Automation & Test in Europe Conference & Exhibition (DATE 2010), pp 1341\u20131344","DOI":"10.1109\/DATE.2010.5457017"},{"key":"630_CR15","doi-asserted-by":"crossref","unstructured":"Kuhlmann M, Gogolla M, France RB, Kazmeier J, Breu R, Atkinson C (2012) From uml and ocl to relational logic and back. In: France RB, Kazmeier J, Breu R, Atkinson C (eds) Model driven engineering languages and systems, Springer, Berlin, Heidelberg, pp 415\u2013431","DOI":"10.1007\/978-3-642-33666-9_27"},{"key":"630_CR16","doi-asserted-by":"crossref","unstructured":"Torlak E, Jackson D (2007) Kodkod: a relational model finder. Tools and Algorithms for the Construction and Analysis of Systems: 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24-April 1, 2007. Proceedings 13, Springer, pp 632\u2013647","DOI":"10.1007\/978-3-540-71209-1_49"},{"key":"630_CR17","doi-asserted-by":"crossref","unstructured":"Nijjar J, Bultan T (2012) Unbounded data model verification using smt solvers. 2012 Proceedings of the 27th IEEE\/ACM International Conference on Automated Software Engineering, pp 210\u2013219","DOI":"10.1145\/2351676.2351706"},{"key":"630_CR18","doi-asserted-by":"crossref","unstructured":"Cabot J, Claris\u00f3 R, Riera D (2008) Verification of uml\/ocl class diagrams using constraint programming. 2008 IEEE International Conference on Software Testing Verification and Validation Workshop, pp 73\u201380","DOI":"10.1109\/ICSTW.2008.54"},{"key":"630_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jss.2014.03.023","volume":"93","author":"J Cabot","year":"2014","unstructured":"Cabot J, Claris\u00f3 R, Riera D (2014) On the verification of uml\/ocl class diagrams using constraint programming. J Syst Softw 93:1\u201323","journal-title":"J Syst Softw"},{"key":"630_CR20","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1016\/j.is.2018.08.005","volume":"81","author":"B P\u00e9rez","year":"2019","unstructured":"P\u00e9rez B, Porres I (2019) Reasoning about uml\/ocl class diagrams using constraint logic programming and formula. Inf Syst 81:152\u2013177","journal-title":"Inf Syst"},{"key":"630_CR21","doi-asserted-by":"crossref","unstructured":"Jackson E, Schulte W (2013) Formula 2.0: a language for formal specifications. Unifying Theories of Programming and Formal Engineering Methods, Springer, Berlin Heidelberg, pp 156\u2013206. https:\/\/www.microsoft.com\/en-us\/research\/publication\/formula-2-0-language-formal-specifications\/","DOI":"10.1007\/978-3-642-39721-9_4"},{"key":"630_CR22","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2023.102955","volume":"228","author":"H Wu","year":"2023","unstructured":"Wu H (2023) Qmaxuse: a new tool for verifying uml class diagrams and ocl invariants. Sci Comput Program 228:102955","journal-title":"Sci Comput Program"},{"key":"630_CR23","doi-asserted-by":"publisher","first-page":"1271","DOI":"10.1007\/s10270-020-00849-8","volume":"20","author":"H Wu","year":"2021","unstructured":"Wu H, Farrell M (2021) A formal approach to finding inconsistencies in a metamodel. Softw Syst Model 20:1271\u20131298","journal-title":"Softw Syst Model"},{"key":"630_CR24","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.scico.2007.01.013","volume":"69","author":"M Gogolla","year":"2007","unstructured":"Gogolla M, B\u00fcttner F, Richters M (2007) Use: a uml-based specification environment for validating uml and ocl. Sci Comput Program 69:27\u201334","journal-title":"Sci Comput Program"},{"key":"630_CR25","unstructured":"Gogolla M, Hilken F (2016) In Model validation and verification options in a contemporary uml and ocl analysis tool Modellierung 2016, Gesellschaft f\u00fcr Informatik e.V, Bonn, pp 205\u2013220"},{"key":"#cr-split#-630_CR26.1","doi-asserted-by":"crossref","unstructured":"Maoz S, Ringert JO, Rumpe B, Mezini M (2011) CDDiff: semantic differencing for class diagrams. In: Mezini M","DOI":"10.1007\/978-3-642-22655-7_12"},{"key":"#cr-split#-630_CR26.2","unstructured":"(ed) ECOOP 2011 - Object-Oriented Programming, Springer, Berlin Heidelberg, pp 230-254"},{"key":"630_CR27","unstructured":"Jackson D (2006) Software abstractions: logic, language, and analysis, The MIT Press"},{"key":"630_CR28","unstructured":"Kautz O, Maoz S, Ringert JO, Rumpe B (2017) CD2Alloy: a translation of class diagrams to alloy. Technical Report AIB-2017-06, RWTH Aachen University"},{"key":"630_CR29","unstructured":"Nachmann I, Rumpe B, Stachon M, St\u00fcber S (2022) Open-World loose semantics of class diagrams as basis for semantic differences. Modellierung 2022, Gesellschaft f\u00fcr Informatik e.V., pp 111\u2013127"},{"key":"630_CR30","doi-asserted-by":"crossref","unstructured":"Drave I, Kautz O, Michael J, Rumpe B, Berger T et\u00a0al (2019) Semantic evolution analysis of feature models. In: Berger T. et\u00a0al (eds) International systems and software product line conference (SPLC\u201919), ACM, pp 245\u2013255","DOI":"10.1145\/3336294.3336300"},{"key":"630_CR31","doi-asserted-by":"crossref","unstructured":"Maoz S, Ringert JO, Rumpe B (2011) ADDiff: semantic differencing for activity diagrams. Conference on foundations of software engineering (ESEC\/FSE \u201911), ACM, pp 179\u2013189","DOI":"10.1145\/2025113.2025140"},{"key":"630_CR32","unstructured":"Maoz S, Ringert JO, Rumpe B. An Operational Semantics for Activity Diagrams using SMV. Technical Report AIB-2011-07, RWTH Aachen University, Aachen, Germany (2011)"},{"key":"630_CR33","unstructured":"Kautz O, Rumpe B (2018) Semantic Differencing of Activity Diagrams by a Translation into Finite Automata. Proceedings of MODELS 2018. Workshop ME"},{"key":"630_CR34","doi-asserted-by":"crossref","unstructured":"Drave I, Eikermann R, Kautz O, Rumpe B, Hammoudi S, Pires LF, Seli\u0107 B (2019) Semantic differencing of statecharts for object-oriented systems. In: Hammoudi S, Pires LF, Seli\u0107 B (eds) In: Proceedings of the 7th International Conference on Model-Driven Engineering and Software Development (MODELSWARD\u201919), SciTePress, pp 274\u2013282","DOI":"10.5220\/0007351902740282"},{"key":"630_CR35","unstructured":"Kautz O (2021) Model analyses based on semantic differencing and automatic model repair aachener informatik-berichte, Software Engineering, Band 46, Shaker Verlag"},{"key":"630_CR36","doi-asserted-by":"crossref","unstructured":"Butting A, Kautz O, Rumpe B, Wortmann A (2017) Semantic differencing for message-driven component & connector architectures. International conference on software architecture (ICSA\u201917), IEEE, pp 145\u2013154","DOI":"10.1109\/ICSA.2017.34"},{"key":"630_CR37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22413-3","volume-title":"Modellierung mit UML","author":"B Rumpe","year":"2011","unstructured":"Rumpe B (2011) Modellierung mit UML, 2te edn. Springer, Berlin","edition":"2te"},{"key":"630_CR38","unstructured":"Cengarle MV, Gr\u00f6nniger H, Rumpe B (2008) System Model Semantics of Class Diagrams. Informatik-Bericht 2008-05, TU Braunschweig, Germany"},{"key":"630_CR39","doi-asserted-by":"crossref","unstructured":"Fahrenberg U, Acher M, Legay A, Wasowski A Gnesi S, Rensink A (2014) Sound merging and differencing for class diagrams. In: Gnesi S, Rensink A (eds) Fundamental approaches to software engineering, Springer, Berlin, Heidelberg, pp 63\u201378","DOI":"10.1007\/978-3-642-54804-8_5"},{"issue":"2","key":"630_CR40","first-page":"1","volume":"22","author":"A Lindt","year":"2023","unstructured":"Lindt A, Rumpe B, Stachon M, St\u00fcber S (2023) CDMerge: semantically sound merging of class diagrams for software component integration. J Object Tech (JOT) 22(2):1\u201314","journal-title":"J Object Tech (JOT)"},{"key":"630_CR41","doi-asserted-by":"crossref","unstructured":"Cook SA (1971) The complexity of theorem-proving procedures. Proceedings of the third annual ACM symposium on Theory of computing, pp 151\u2013158","DOI":"10.1145\/800157.805047"},{"key":"630_CR42","doi-asserted-by":"crossref","unstructured":"Mukherjee R, Kroening D, Melham T (2015) Hardware verification using software analyzers. 2015 IEEE Computer Society Annual Symposium on VLSI, IEEE, pp 7\u201312","DOI":"10.1109\/ISVLSI.2015.107"},{"key":"630_CR43","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1145\/2090147.2094081","volume":"10","author":"P Godefroid","year":"2012","unstructured":"Godefroid P, Levin MY, Molnar D (2012) Sage: whitebox fuzzing for security testing: sage has had a remarkable impact at microsoft. Queue 10:20\u201327","journal-title":"Queue"},{"key":"630_CR44","doi-asserted-by":"crossref","unstructured":"Tillmann N, De\u00a0Halleux J (2008) Pex\u2013white box test generation for. net. Tests and Proofs: Second International Conference, TAP 2008, Prato, Italy, April 9-11, 2008. Proceedings 2, Springer, pp 134\u2013153","DOI":"10.1007\/978-3-540-79124-9_10"},{"key":"630_CR45","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner N, Jayaraman K (2015) Checking cloud contracts in microsoft azure. Distributed Computing and Internet Technology: 11th International Conference, ICDCIT 2015, Bhubaneswar, India, February 5-8, 2015. Proceedings 11, Springer, pp 21\u201332","DOI":"10.1007\/978-3-319-14977-6_2"},{"key":"630_CR46","unstructured":"Gamma E, Johnson R, Helm R, Johnson RE, Vlissides J (1995) Design patterns: elements of reusable object-oriented software, Pearson Deutschland, GmbH"},{"key":"630_CR47","doi-asserted-by":"crossref","unstructured":"Barrett C, et\u00a0al (2011) Cvc4. International conference on computer aided verification, Springer, pp 171\u2013177","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"630_CR48","doi-asserted-by":"crossref","unstructured":"Deters M, Reynolds A, King T, Barrett C, Tinelli C (2014) A tour of cvc4: how it works, and how to use it. 2014 Formal Methods in Computer-Aided Design (FMCAD), IEEE, pp 7\u20137","DOI":"10.1109\/FMCAD.2014.6987586"},{"key":"630_CR49","doi-asserted-by":"crossref","unstructured":"Bansal K, Reynolds A, Barrett C, Tinelli C (2016) A new decision procedure for finite sets and cardinality constraints in smt. Automated Reasoning: 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27\u2013July 2, 2016, Proceedings, Springer, pp 82\u201398","DOI":"10.1007\/978-3-319-40229-1_7"},{"key":"630_CR50","doi-asserted-by":"crossref","unstructured":"Rumpe B (2012) Agile Modellierung mit UML: codegenerierung, Testf\u00e4lle, Refactoring, 2nd edn. Springer, Berlin","DOI":"10.1007\/978-3-642-22430-0_1"},{"key":"630_CR51","unstructured":"Ahn G-J, Shin ME (2001) Role-based authorization constraints specification using object constraint language. Proceedings Tenth IEEE International Workshop on Enabling Technologies: Infrastructure for Collaborative Enterprises. WET ICE 2001, IEEE, pp 157\u2013162"}],"container-title":["Innovations in Systems and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-026-00630-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11334-026-00630-y","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11334-026-00630-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,22]],"date-time":"2026-06-22T03:48:13Z","timestamp":1782100093000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11334-026-00630-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,5,25]]},"references-count":52,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2026,6]]}},"alternative-id":["630"],"URL":"https:\/\/doi.org\/10.1007\/s11334-026-00630-y","relation":{},"ISSN":["1614-5046","1614-5054"],"issn-type":[{"value":"1614-5046","type":"print"},{"value":"1614-5054","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,5,25]]},"assertion":[{"value":"15 January 2025","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"12 April 2026","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 May 2026","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}},{"value":"Not applicable","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethics approval and consent to participate"}},{"value":"Present","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Consent for publication"}},{"value":"Available on Github, see section","order":5,"name":"Ethics","group":{"name":"EthicsHeading","label":"Materials availability"}},{"value":"Available on Github, see section","order":6,"name":"Ethics","group":{"name":"EthicsHeading","label":"Code availability"}}],"article-number":"14"}}