Incremental Verification of UML/OCL Models

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.