A Technique for Automatic Validation of Model Transformations

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

26 Citations (Scopus)


We present in this paper a technique for proving properties about model transformations. The properties we are concerned about relate the structure of an input model with the structure of the transformed model. The main highlight of our approach is that we are able to prove the properties for all models, i.e. the transformation designer may be certain about the structural soundness of the results of his/her transformations. In order to achieve this we have designed and experimented with a transformation model checker, which builds what we call a state space for a transformation. That state space is then used as in classical model checking to prove the property or, in case the property does not hold to produce a counterexample. If the property holds this information can be used as a certification for the transformation, otherwise the counterexample can be used as debug information during the transformation design process.
Original languageUnknown
Title of host publicationLecture Notes in Computer Science
Publication statusPublished - 1 Jan 2010
EventModel Driven Engineering Languages and Systems (MODELS) -
Duration: 1 Jan 2010 → …


ConferenceModel Driven Engineering Languages and Systems (MODELS)
Period1/01/10 → …

Cite this