Semantic Difference Analysis with Invariant Tracing for Class Diagrams Extended by OCL

Models are the primary source-artifacts in Model Driven Development (MDD) 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 Satisfiability Modulo Theories (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. Additionally, invariants are traced across models. The implementation of this tool is publicly available.