Would you like to ensure that you wrote a transformation correctly, but are disappointed with the current no tool support for the V&V of model transformations? Keep reading to see how the SEET tool can help you in this regard.

Model transformations are the cornerstone of any Model-Driven Engineering (MDE) approach. But even if you don’t get any syntax or runtime error when trying your transformation, you cannot be 100% sure that it’s free from logical errors.

Logical errors in model transformations

By logical error we mean an error in the program which causes an undesirable output or runtime error. Consider the following example which is part of the Families2Persons transformation. It has no compile-time or runtime error, but still, it is not correct. The logical error is in line 15; the return value of the isFemale operation must be “true” for a daughter.

1 rule Member2Male
2 	transform s : Families!Member
3 	to t : Persons!Male {
4
5 	guard : not s.isFemale()
6
7 	t.fullName = s.firstName + " " + s.familyName();
8 }
9
10 operation Families!Member isFemale() : Boolean {
11 	if (self.familyMother.isDefined()) {
12 		return true;
13 	} else {
14 		if (self.familyDaughter.isDefined()) {
15 			return false;
16 		} else {
17 			return false;
18		}
19 	}
20 }

In such a case, it is a waste of time to manually check whether the transformation is correct or not. We need a tool to help us in this regard. Some black-box approaches have been presented. However, they may generate duplicate test cases. We propose to use a symbolic execution technique, a proven technique in software engineering, to find logical errors in model transformations.

We focus on ETL transformations, as ETL is one of the most popular model transformation languages in the community.  However, we can apply the same approach to other similar rule-based model transformation languages.

Symbolic Execution of a Transformation

To understand the main idea behind SEET, consider Figure 1, which compares concrete and symbolic executions of programs vs. transformations. For symbolic execution of programs, the level of abstraction is increased by giving symbolic values to the program, and producing symbolic expressions as the output.

As can be seen, instead of 6 in the output, we have A+B+C. Similarly, for symbolic execution of model transformations, only the source and target metamodels are required as inputs (no input model is required). The output for this process is a subset of symbolic target metamodel which we call it Symbolic Metamodel Footprint (SMF). The SMF is a subset of the target metamodel whose attributes have symbolic values. By way of illustration, instead of having a Female class with fullname ‘Ana Smith’, we have ‘Member.firstName Member.familyMother.lastName’. Admittedly, only model elements which appear in the transformation can appear in the SMF. In such a model, there exists at most one class for each of the target metamodel classes. The relations in SMF are slightly different than the relations in the target metamodel, e.g., the inheritance relation does not exist in SMF.

Symbolic exectuion of transformations

Figure 1. Concrete and symbolic execution of programs vs. transformations

The SEET approach

SEET can detect over fifty kinds of errors in ETL transformations. In a black-box view, SEET takes the ETL transformation definition along with source and target metamodels as inputs and generates an SMF, the path condition, and the test model as outputs. In case the expected output model has been provided, the result of the correctness of the transformation is specified as well.

The methodology of SEET can be seen in Figure 2. It consists of 8 main steps as follows.

The SEET approach for symbolic execution of ETL transformations

Figure 2. The SEET approach for symbolic execution of ETL transformations

  1. The ETL code is transformed to its equivalent ETL transformation model by using Haetae.
  2. Our ETL CFG generator, which is an independent tool, produces the CFG of the ETL transformation from its transformation model.
  3. The symbolic execution engine takes the generated CFG along with the ETL transformation model and the source and target metamodels as input to navigate the transformation model. During its operation, if necessary, the engine uses the symbol table and traceability links. By symbolically executing each statement, the SMF is gradually generated. You can see a sample of SMF in Figure 3.

    Figure 3. The SMF of the Families2Persons transformation when member is mother

  4. When a condition is encountered, the path condition generator calculates two path conditions (PCs).
    PC1 = Condition ^ PC
    PC2 = (~ Condition) ^ PC
  5. The path condition evaluator checks whether these PCs are satisfiable. As shown in Figure 4, this is done by first checking the containment preservation. To clarify, for the Families2Persons transformation, the containment preservation unit checks 1) a Member cannot be mother and daughter at the same time, 2) a Member has one of the father, mother, daughter, or son role. If the check is passed, the PCs are checked via AnATLyzer as well.

    Figure 4. The path condition evaluation unit

    In case one of the PCs cannot be met, the execution will be continued through the satisfiable one.

  6. If both path conditions are met, depending on the symbolic execution mode, the engine adopts a different approach. In the interactive mode, after preparing the corresponding part of the transformation model, the tool interacts with the tester and the execution will be continued with the path specified by the tester (Figure 5). In case of selecting the automatic mode, the engine considers both paths.

    Figure 5. Encountering condition in the path in the interactive mode

  7. When the transformation statements are exhausted, the Conformance checker checks whether the SMF conforms to the target metamodel. What we mean by conformance is as follows.
  • All classes of the SMF exist in the target metamodel.
  • All its attributes and references exist in the attributes and references of the corresponding class in the target metamodel or in its parents in a hierarchy.

In case the generated SMF does not conform to the target metamodel, it is discarded. Otherwise, SEET provides test models for each execution path.

  1. The tester ensures the correctness of the transformation by considering the SMF or giving the expected SMF to SEET so that in step 8, its symbolic oracle specifies whether the transformation is implemented correctly.

 

Tool support

The open-source SEET tool that is built based upon these ideas as well as a tutorial on how to use SEET is available on Github. You can see some screenshots of the tool next.

Tool support for the Symbolic execution of transformations

Figure 6. The SEET tool

To evaluate the approach, we have provided some mutants for ETL transformations. You can access them through Github as well.

Additional information

Interested in modeling?

Interested in modeling?

Follow the latest news on software modeling and low-code development

You have Successfully Subscribed!

Pin It on Pinterest

Share This