Tools and resources for verifying model transformations through OCL contracts

The archive is an Eclipse workspace containing projects implementing the contract example on the interface addition refinement and also the tools presented in the OCL 09 workshop paper. It also presents another example: the accessor addition for attributes.

Our tools are currently prototypes that implement the features we presented, but we are still working on them to correct some bugs (see below).

OCL contracts are checked through an ATL dedicated transformation integrating the OCL invariants representing the contracts. A global verification result is generated but finest verification results for specific elements can also be generated, depending on the contract implementation.

Workspace contents

The workspace contains 3 projects:

Contract validation

For checking the contrat concerning the element evolution between the source and the target models, one have to begin to obtain these two models. For that, models of the folder models of project ClassDiagram can for instance be used and modified. A transformation, the automatic interface addition for instance, can then be applied through the transformations of the project Transformations. Then, through our mapping function tool, the global model concatenating these two models is created.

Then, one can apply the transformation InterfaceContractEvolution.atl or UnModificationContract.atl on this model. The generated model will detail the contract evalution result: it will inform if all elements respect the contract.

For an easy test of the contract respect, just use an already generated model concatenation file (ModelConcatInterface.xmi for instance) and modify it directly.

The UnModificationContract.atl file has been fully automatically generated with our mapping function generation tool (with little modifications of the ATL rules to add the element names in the generated result).

Mapping function generator and associated tools

For using the mapping function generator, just execute the MappingFunctions.jar jar file of the tools folder of the ClassDiagram project (this jar file may also or only appear in the Referenced Libraries folder).

Then, clik on "Load MetaModel" for loading an Ecore meta-model. List of elements of the meta-model will appear on the left. When selecting one element, a tree containing its attributes and references to other elements is available on the right part. Select the attribute and reference you want and click on:

The tool proposes two other tabs:

To use these features, just fill the required file name and execute the associated action.

TODO: bugs to fix or features to implement

Used versions

Eclipe : Ganymede (3.4)
ATL : 2.0.1
Kermeta : 1.2.0


Eric Cariou, last modification : 02/10/09