Two Basic Correctness Properties for ATL Transformations: Executability and Coverage

Elena Planas talks about our joint work (together with Cristina Gómez) about two basic correctness properties easy to check on your ATL transformations:

Model transformations play a cornerstone role with the emergence of Model Driven Engineering (MDE), where models are transformed from higher to lower levels of abstraction. Unfortunately, a quick and easy way to check the correctness of model transformations is still missing, which compromises their quality (and in turn, the quality of the target models generated from them).

As a solution, in the paper presented in MtATL 2011 workshop we propose a lightweight method that performs a static analysis of ATL rules with respect to two correctness properties: weak executability and coverage. In order to improve its efficiency, our method works at design time without any need to simulate/execute the rules. A relevant feature of our method is the feedback it provides: if the checked property is not satisfied, the method returns feedback suggesting possible corrections to repair the detected errors.

First property we propose, weak executability of an ATL rule r, analyzes whether a rule r may be safely applied without breaking the target metamodel integrity constraints. That is, if there is at least a given set of elements that matches the input pattern of r and for which the execution of  r generates a target model consistent with the target metamodel and its integrity constraints. Otherwise r is useless, as every time it is executed, an error arises because the target model violates some integrity constraints.

As an example, consider the ATL rule “Person2Student” (which transforms people into students) according to the source and target metamodels showed below:

module Person2Student;

create OUT: StudentMM from IN: PersonMM;

rule Person2Student {
	from p: PersonMM!Person
	to s: StudentMM!Student (
		fullName <-,
		college <- c
	c: StudentMM!College (
	name <- p.collegeName


Rule “Person2Student” is not weakly executable since, every time we create a new student and we do not associate it to any subject, we reach an erroneous target model where the minimum 1 cardinality of the IsEnrolledIn association is violated given that the new student is not related with any subject. Our method can report that, in order to create a new student, we need to assign at least one subject within the same execution.

The second property we propose, covering of an ATL rule set, analyzes whether a set of rules allow addressing all elements of the source and target metamodels. This property may be viewed regarding two perspectives:

  • Source-coverage: We consider that a set of ATL rules is source-covering when all elements of the source metamodel may be navigated through the execution of these rules. For instance, the set composed by the single rule “Person2Student” is not source-covering since, for instance, rules to navigate age attribute and Knows association are not specified.
  • Target-coverage: We consider that a set of ATL rules is target-covering when all elements of the target metamodel may be created and initialized through the execution of these rules. For instance, the set composed by the single rule “Person2Student” is neither target-covering since, for instance, rules to create objects of type Subject are not specified, forbidding users to create new subjects on the target model.

Even though not coverage does not indicate explicitly an error but only a warning, we feel this property is important to guarantee that no behavioral elements are missing in the rules.

For more information about how our method computes weak executability and coverage properties in a static way, please, read the complete paper.

If you enjoyed this post you can subscribe to this Software Modeling blog , to the portal’s mailing list , follow me on twitter and/or participate in the forums . And if you really liked it help me pass it on to others by sharing the post using the links below. Don’t forget to check our

3 Responses to Two Basic Correctness Properties for ATL Transformations: Executability and Coverage

  1. Hi,
    After your previous post ( ) y quickly scanned the papers and this was one of the three that I downloaded in my “To read” folder. Definitely interesting, congratulations.
    I would like to apply the method to assess a set of ATL rules in my PhD. However, I’m under quite a lot of pressure to finish the draft, so it may remain as future work after all.
    I just wonder how scalable the method is without proper tool support. My metamodels and the set of rules are not enormous but it nay be tough to apply to them.

  2. Elena Planas says:

    Thank you Sergio. Certainly, applying our method without tool supoort may be a bit tedious and hard. In fact, as a further work, we plan provide tool support for the method. Once implemented, it would be very useful to validate our method using your rules!

    In the same line, I would also like to mention the work presented by Marcel van Amstel and Mark van der Brand in ICMT2011, where they presented a method and a tool (which provides visual feedback) to check a property similar to our coverage. It would be very helpful to integrate all the existing analysis techniques to provide a framework for analyzing the correctness of ATL rules regarding several properties.

  3. [...] = 'wpp-261'; var addthis_config = {"data_track_clickback":true};Related to the previous post on the static verification of transformations, now Elena explains how to check the quality of your executable UML models for instance written [...]

Leave a Reply

Your email address will not be published. Required fields are marked *

You may use these HTML tags and attributes: <a href="" title=""> <abbr title=""> <acronym title=""> <b> <blockquote cite=""> <cite> <code> <del datetime=""> <em> <i> <q cite=""> <strike> <strong>

Powered by WordPress
More in transformations
Learn MoDisco, ATL, EMF Facet and EEF
A Perl implementation of the UML metamodel

Summary of the 2nd day of the Int. Conf. on Model Transformation 2011