Introduction

As model-driven engineering (MDE) is progressively being adopted by industry, model transformations (MT) are becoming commonplace. Their complexity is also growing, since the problems they need to deal with are increasingly harder. From simple structural migration, model queries or pattern-based code-generation, they now have to cope with complex model synthesis, behavioural analysis and stream data processing. This has led, among other things, to the need of engineering model transformations [7].

In this context, the specication of a model transformation becomes a critical task, in particular for checking the correctness of its implementations. Please note that correctness is not an absolute property, but needs to be checked against a contract, or specication, which determines the expected behaviour, the context whether such a behaviour needs to be guaranteed, as well as some other properties of interest. The specication states what should be done, but without determining how. The problem, again, is that the specication of a model transformation can be as complex as the transformation itself.

Here we will make use of the fact that, in essence, a model transformation is an algorithmic specication (either declarative or operational) of the relationship between two or more models, and more specically, of the mapping from one model to another [12]. Thus, one way to specify a model transformation is by means of a transformation model that denes such a relation [3].

In this paper we propose an iterative process for the correct specication of model transformations, i.e., for developing correct transformation models. This is done by testing the relationship specied by the transformation. We use classifying terms [5] to implement a divide-and-conquer strategy that permits simplifying the analysis of the mappings established by the model transformation, by focusing on particular input models. This approach is based on the ideas proposed by equivalence partitioning, a software testing technique that divides the input data of a software unit into partitions of equivalent data from which test cases can be derived. Once a problem is detected, the specication is revised to solve it. This process is iterated until the specication is found free of errors.

One additional benet of our approach, and a dierence with regard to previous proposals, is that it permits testing the specication without needing an implementation of the model transformation, which is the common way in which model transformation specications and implementations are tested (by checking one against the other, i.e., using a particular kind of redundancy testing). In our approach, model transformation specications can be tested on their own, before any implementation is available.

Preliminaries

Here, we develop a transformation model using a test-driven approach. Assisted by a model validator that completes partial object diagrams to consistent system states, bugs in the model description are identied and the transformation model is iteratively xed until it is complete, works as expected and no more bugs can be detected.

Running Example

The two initial models, the transformation is developed for, are simple bibliography managers shown in Fig. 1.

One resembles the information of BibT E X les and the other resembles the DocBook format. At the top of the structure is the BibTeXFile or the DocBook with entries for proceedings and inproceedings that will be mapped to books and articles, respectively. Additionally, authors and editors are saved.

Dierences in the models exist in the structure how the information is saved and the capabilities saved information. For instance, the BibT E X model saves the year of the event (yearE) and the year of publication (yearP)

for proceedings, which are not present in the DocBook model. Therefore, the transformation model will not be able to cover all attributes of the models.

Characteristics of Classifying Terms

Classifying terms [5] are an instrument to explore model properties. They are employed in the model validation and verication process when one has a UML and OCL model given, and one has in addition a so-called conguration that species a nite search space connecting the models elements, basically classes, associations, attributes, and datatypes, with nite sets of possible populations. As an important validation task, the developer might want to see all object models that satisfy the UML and OCL class model and that t to the conguration.

Classifying terms give the developer an explicit option to formulate their understanding of two object models being dierent. Thus when the developer scrolls through all object models matching the UML class model, the OCL invariants and the conguration, they will only encounter models with dierent characteristics with respect to the classifying term.

The technical realization works as follows. The developer species a closed OCL query term, i.e., a term without free variables, that can be evaluated in an object model and that returns a characteristic value. This term is called `classifying term'. Each newly constructed object model has to show a dierent characteristic value for the classifying term. The classifying term determines an equivalence relationship on all object models. Two object models with the same characteristic value belong into the same equivalence class. Our approach decides to choose only one representative from each equivalence class.

The denition of the classifying terms corresponds to the mapping that the developer has in mind about the transformation, and how it should map source models of each source equivalence class into target models of the corresponding target class. In this sense, the source and target classifying terms should be `in correspondence'.

Our approach can also help checking such expected mappings.

Test Case Generation with Classifying Terms

In order to eciently test our transformation model, we create test cases using classifying terms. This technique results in test cases covering developer chosen equivalence classes that are determined by the classifying terms.

As a result, exactly one test case is automatically generated for each equivalence class. They have a much broader coverage than only few manual tests. Depending on a clever choice for the classifying terms, the advantages are faster test execution, due to a smaller test suite, as well as a higher error detection rate per test case that cover many, if not all, errors already.

We dened three classifying terms for the source metamodel and three for the target metamodel of our running example. They infer eight equivalence classes in each one. The source classifying terms focus on dierent characteristics of the input models of the transformation. First, we want to have input models in which proceedings have dierent conference event and publication years, and other in which they coincide. Second, we want to have some sample input models in which two editors of proceedings invite the other to have a paper there; respectively, we also want to have input models in which this manus-manum-lavat situation does not happen. Finally, we want to have some source models with proceedings edited by one of the authors of the papers in the proceedings, and other input models with no self-edited proceedings:

[ yearE_EQ_yearP ] Proc.allInstances->forAll(yearE=yearP) The classifying terms for the target models identify properties of interest in the target space, such as self-edited books, or books which are authored by a single person. They are not shown here for space reasons. Several problems can be easily detected. First of all, there is no one-to-one correspondence between the source and target objects: the target contains more objects than it should. This does not match with the expected behaviour of the transformation, which should establish a one-to-one relation between the source and target model elements. We can make use of the fact that at the specication level, the relationship established by the transformation can be read and traversed in both ways, i.e., the transformation model is direction-neutral. Then, we manually created the expected target object diagram (left-hand side of Fig. 4) and completed it. The result after the completion is shown in the right-hand side of Fig. 4, where we can see that the source model obtained is not the third object diagram obtained applying the classifying terms (the objects inside the square in Fig. 3), which means that the transformation model, as it is, does not establish the expected relationship between the source and target model elements. This problem is solved by adding object equality to the constraints to limit the number of objects generated when completing the object diagrams. 1 The changes made in the specication are highlighted with a gray background. Another observable problem is that the names were supposed to be unique i.e., a DocBook should not have two Books with the same name and a Book should not have two Articles with the same name but they are not. In the constraints the one operation, which is intended for the uniqueness, is placed inside the body of an exists operation, which leads to the situations shown in Fig. 3. In the object diagram there are two DocBooks but only one of them respects the uniqueness (docBook2). As there exists one DocBook object fullling the constraint, the overall system state is valid. In order to achieve the desired behaviour, the exists expressions need to be replaced by one expressions. After the two changes the constraints look like the following. 4 Related Work

[

In the eld of Model-Driven Engineering, model transformations are key elements and even the simplest ones may contain faults as pointed in [11]. Therefore, their testing, validation and verication have been subject of investigations. In this work, we see model transformations as transformation models and, as a software artifact, there exists the need of checking their correctness as well.

Several lines of work consider the testing of model transformation implementations. Some of them are dynamic approaches that execute the model transformations given an input model or a set of them. References [9] and [13] present a contribution for debugging model transformations. The work in [1] analyses the trace model in order to nd errors. Also, Tracts [12] are a static black-box approach that establishes contracts between the source and target metamodels which dene the transformation specication. They have been combined with classifying terms in [5] for automatically constructing relevant source model test cases. In addition to Tracts, other static approaches have been proposed [8] that allow the specication of contracts in a visual manner, and the work in [4] that looks at the dierences between the actual output model generated by the transformation and the expected output model.

Reference [2] proposes a dynamic testing technique dening equivalence classes for the source models in a similar manner as it is done with classifying terms. Nevertheless, their proposal is less expressive as they do not consider the use of OCL, less exible and lacks full automation. Reference [6] presents a mechanism for generating test cases by analysing the OCL expressions in the source metamodel in order to partition the input model space. This is a systematic approach similar to ours, but focusing on the original source model constraints.

Our proposal allows the developer partitioning the source (and target) model space independently from these constraints, in a more exible manner.

Finally, the work in [10] proved the correctness of specications by making use of algebras. Our approach can be seen as a rst step and as an easier and cheaper way that does not require for the developer to have any extra knowledge or create any other software artifact.

Conclusion and Future Work

In this paper we have presented an iterative approach for the correct development of transformation models.

These models provide the specications of model transformations, and with our proposal they can be checked before any implementation is available, and independently from any of them.

There are several lines of work that we plan to address next. In the rst place, we would like to validate our proposal with more transformations, in order to gain a better understanding of its advantages and limitations; identify dierent contexts of use in which our approach works well and other in which the results are not satisfactory (and why), and build a repository of thoroughly tested and validated transformation models that can be reused by the community. Second, we plan to improve the tool support to further automate all tests, so human intervention is kept to the minimum. Finally, we need to dene a systematic approach of dening classifying term and transformation model testing using the preliminary ideas outlined in this paper.