Overview

Overview of Echo's features

Echo is a tool for model repair and transformation in the context of model-driven engineering (MDE). The main focuses of Echo are

• correctness, in the sense that all constraints of the system are guaranteed to hold for repaired models;
• least-change, since those repaired models are as close as possible to the original inconsistent ones.

At the core of Echo's repair procedures is the Alloy relational solver, which has support for model checking and model finding.

The constraints supported by Echo are of two kinds:

• intra-model constraints, defined by the conformity of models to their metamodels (possibly with additional constraints);
• inter-model constraints, defined by relations between coexisting models, which give rise to bidirectional transformations.

For both kinds of constraints, Echo is able to both check and repair models, in which case model resources are effectively repaired (as opposed to just proposing abstract repair operations). Despite the repairs being always minimal, the user is able to determine how the distance between the models is calculated. Echo provides two different metrics:

• graph edit distance, which is automatically inferred from the metamodel and is context-oblivious;
• operation-based distance, that is parametrizable by the user through the definition of the valid update steps as operations.

Furthermore, since there may exist multiple consistent models at a minimal distance, Echo presents all valid solutions to the user, allowing him to choose the best-suited one (as opposed to selecting an arbitrary one).

All efforts have been made to integrate Echo seamlessly in the MDE development process. Thus Echo is deployed as a plugin for the popular Eclipse IDE and over the Eclipse Modeling Framework (EMF). It is metamodel independent, processing any user-defined metamodels and corresponding models, and supports standard MDE file formats, mostly prescribed by OMG.

Supported formats

• Metamodels are specified in Ecore (a version of MOF, OMG's meta-metamodel), as specified by the EMF.

• Additional constraints in the metamodel can be defined by embedding OCL (OMG's constraint language) formulas in annotations. This is the same mechanism prescribed by EMF's OCLinEcore.

• Operations (used for the operation-based distance), are also defined by OCL annotations over the operations' specifications.

• Inter-model constraints are specified by QVT Relations (QVT-R) transformations, the language prescribed by OMG to specify model transformations. Well-founded recursion is supported and relations may contain arbitrary OCL constraints both in where and when clauses, as well as in the domain patterns.

• Models are specified as XMI resources, that must conform to an Ecore metamodel.

• The complete subset of the OCL language supported can be consulted in this paper. It includes the transitive closure operator, recently introduced by the OCL standard.

For a more comprehensive presentation of the supported languages, visit this page.

Functionalities

Model visualization

Models are presented using the Alloy visualizer. For better readability, an Alloy theme is automatically inferred from the meta-model, although an user-defined theme can also be provided if desired.

Model generation

Given a meta-model and user-specified size, Echo can generate a new model conformant with the metamodel. Additional OCL constraints can also be specified to generate instances with a parametrized shape.

Consistency check

Given a model, Echo can check if it conforms to the respective meta-model annotated with OCL constraints.

Model repair

Given a model that does not conform to its OCL-annotated meta-model, Echo can find a minimal repair that produces a consistent model.

Inter-model consistency check

Given a QVT-R or ATL transformation and a set of models that are supposed to be consistent via it, Echo can check if such is the case.

Inter-model consistency repair

QVT-R or ATL transformation are interpreted as bidirectional transformations, so that given inconsistent models, Echo is able to repair them in order to recover consistency.

Batch transformation

Given a QVT-R or ATL transformation and existing models, Echo can generate the minimal model consistent with the existing models by the specified transformation.

For more information about how these features are implemented please consult the fundaments of Echo or the scientific publications. To start using Echo, please watch this video or follow this tutorial.