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.