Incremental Verification of UML/OCL Models

By: Robert Clarisó, Carlos A. González, Jordi Cabot

Abstract

Model-Driven Development employs models as core artifacts of the software development process. This requires ensuring the correctness of models, an analysis which is computationally complex. However, models may evolve over time and these changes usually require re-checking models from scratch. To this end, this paper proposes techniques for the incremental verification of a fundamental correctness property: internal consistency of UML class diagrams annotated with OCL constraints. These techniques allow modelers to significantly reduce (or even avoid altogether) the cost of re-verifying a class diagram after model updates.

Keywords

UML, OCL, Formal Verification, Model Evolution, Model Certificate, Scalability

Cite as:

Robert Clarisó, Carlos A. González, Jordi Cabot, “Incremental Verification of UML/OCL Models”, Journal of Object Technology, Volume 19, no. 3 (October 2020), pp. 3:1-16, doi:10.5381/jot.2020.19.3.a7.