On Proving the Correctness of Refactoring Class Diagrams of MDE Metamodels

Abstract

Model Driven Engineering ( MDE ) is a general-purpose engineering methodology to elevate system design, maintenance, and analysis to corresponding activities on models. Models (graphical and/or textual) of a target application are automatically transformed into source code, performance models, Promela files (for model checking), and so on for system analysis and construction. Models are instances of metamodels . One form an MDE metamodel can take is a [class diagram, constraints] pair: the class diagram defines all object diagrams that could be metamodel instances; object constraint language ( OCL ) constraints eliminate semantically undesirable instances. A metamodel refactoring is an invertible semantics-preserving co-transformation, i.e., it transforms both a metamodel and its models without losing data. This article addresses a subproblem of metamodel refactoring: how to prove the correctness of refactorings of class diagrams without OCL constraints using the Coq Proof Assistant.