Tools and resources for verifying model transformations through OCL contracts

The archive ws-contracts.zip 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:

• Project ClassDiagram: contains the definition of the class diagram meta-model, some models and associated tools:
  • Folder metaModels : the class diagram meta-model
    • ClassDiagram.ecore : the meta-model in Ecore
    • ClassDiagramModified.ecore : the same meta-model with addition of the ModelReference class; realized by our meta-model modification tool
    • ClassDiagram.ocl : OCL constraints to supplement the meta-model
    • ClassDiagramTC.ocl : same OCL constraints, in the format expected by the Topcased project OCL checker
    • ClassDiagramUtil.kmt : set of Kermeta operations for manipulating class diagrams (loading, saving, printing, ...)
    • ClassDiagramModified.genmodel : generated "genmodel" of the ClassDiagramModified.ecore, used to generate the model code for manipulating class diagram models in Java
  • Folder models : contain the 3 models given in example in the paper and the model concatenating source and target models of the transformation
    • InitialModel.xmi : initial model
    • IntermediateModel.xmi : model resulting from the automatic transformation of interface addition on the initial model
    • FinalModel.xmi : final model for the interface refinement example, after manual modification of interfaces and methods
    • ModelConcatInterface.xmi : concatenation of the InitialModel.xmi and the FinalModel.xmi models; realized by our concatenation tool
    • InitialModelAccessor.xmi : model resulting from the automatic transformation of accessor addition on the initial model
    • ModelConcatAccessor.xmi : concatenation of the InitialModel.xmi and the InitialModelAccessor.xmi models; realized by our concatenation tool
  • Folder src : contain the EMF model code generated from the ClassDiagramModified.genmodel
  • Folder tools : Java jar files of our tools
    • MappingFunctions.jar : tools allowing mapping function generation, meta-model modification and model concatenation, through one executable Java class: mappingFunctions.MappingFunctionGenerator
    • lablib-checkboxtree-3.0.2.jar : graphical library used by the mapping function generator
• Project Transformations : contain transformations on class diagram models, each one presented in ATL and Kermeta versions:
  • Interface addition refinement: AddInterface.atl and AddInterface.kmt
  • Accessor addition for attributes: AddAccessorRefining.atl and AddAccessorTransfo.kmt
• Project Contracts : contain the contracts, for each transformation, defined through several files:
  • ContractEvaluationResult.ecore : meta-model of contract evaluation result
  • Folder Interface : interface addition refinement contracts
    • InterfaceContractTarget.ocl : OCL constraints on target models
    • InterfaceContractEvolution.atl : OCL constraints on the evolution between source and target models, implemented through an ATL transformation (generate a model of contract evaluation result)
    • ResultInterfaceContract.xmi : result of the evaluation of the evolution constraints on the file ModelConcatInterface.xmi
    • UnModificationContract.atl : OCL constraints for checking the unmodification of some elements of the model (class names, attributes, associations).
    • ResultUnModification.xmi : result of the evaluation of the unmodification constraints on the file ModelConcat.xmi
  • Folder Accessor : attribute accessor contract
    • AccessorContract.atl : contract checking that each attribute has a setter and a getter on the target model and that no attribute has been modified, deleted or added during the transformation.
    • ResultAccessorContract.xmi : result of the evaluation of the attribute contract on the file ModelConcatAccessor.xmi

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:

• OCL Code: for generating mapping functions in standard OCL
• ATL Code: for generating mapping functions in OCL with the ATL syntax and also generating default ATL rules for checking element validity
• ATL File: generates the same OCL functions and rules as for "ATL Code" but saves it in a file named MappingContract.atl in the desired folder. This file contains a complete ATL transformation directly executable. You can use it to define the base of a contract and then rename and modify it.

The tool proposes two other tabs:

• Merge Models: for concatenating a source and a target models into a third global one
• Modify MetaModel: for modifying a meta-model before concatenating models conformed to it

TODO: bugs to fix or features to implement

• Better management of NS URI for models. Currently, before doing the concatenation, source and target models have to be modified by hand to set the correct reference to the meta-model, the modified one instead of the original one.
• Better management of the generated modified meta-models, by notably automatically generates their associated genmodel and model code.
• Fix the bug in Kermeta operations dedicated to the class diagram meta-model: when a method has more than one parameter, the saving of a model fails
• Fix the problems during concatenation of models when one of the model has been generated through a Kermeta transformation
• Improvment of the GUI of the tool

Used versions

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

Developpers

• Definition of the meta-model, tranformations and contracts: Eric Cariou
• Model concatenation tool: Eric Cariou (based on code written by Julien Hadba and Bastien Sabos)
• Mapping function generator: Nidal Djemam, modified by Eric Cariou

Eric Cariou, last modification : 02/10/09