User Manual

As shown in Figure 1, by right clicking on an etl file and selecting the "SEET" option from a popup menu, the tool will be executed.

In the beginning, the configuration wizard is shown to the tester. As can be seen in Figure 2 the tester configures by selecting source and target metamodels. In this case, the symbolic execution of the transformation is started.

Following the configuration, the tester is asked to select a mode. If the tester selects the automatic mode, SEET traverses executable path of the transformation automatically. Otherwise, in the case that the tester selects the interactive mode, satisfiability of conditions is determined by the tester's control.

Consider the case that the tester would selected automatic mode (Figure 3).

In case the wizard of Figure 4 is shown, that means the transformation has been written incorrectly.

Otherwise, to determine the correctness of the transformation, the generated Symbolic Metamodel Footprint (SMF) must be checked. Therefore, the result involving all satisfiable path conditions and their corresponding test models is shown to the tester (Figure 5). For each path condition, its corresponding SMF is generated.

The tester can click on "Finish" and investigate the SMF such that the final correctness of the ETL transformation is specified. To this end, the tester right clicks on the transformation folder and clicks “Refresh.” Then, the tester opens "SMF.model" and "PC.txt" files. PC.txt contains satisfiable path conditions and SMF.model contains their corresponding symbolic output. By checking these two files in the following manner, the tester can determine whether or not the transformation is written correctly.

Assuming in the PC.txt file, we have the below path condition.

Path Condition1: Member.allInstances() -> size() <> 0 and Member.familyMother.isDefined() and
not Member.familyFather.isDefined()

The Member.allInstances() -> size() <> 0 condition means the family has a member. The Member.familyMother.isDefined() condition means the member is the mother of the family. The not Member.familyFather.isDefined() condition means the member is not father. In the SMF.model file, find the package with the corresponding number. Since this is “Path Condition1”, open “Target1” package (Figure 6).

According to the path condition and the transformation aim, we expect to have the following in the Target1 package.

1. Since the family has a member, Target1 package must not be empty.
2. Since the member is a mother, we expect to have Female.
3. The Female must have a fullName attribute.
4. The fullName attribute must have a Member.firstName Member.familyMother.lastName value.

If at least one of the above conditions is not satisfied, stop checking other path conditions and packages and specify the transformation as faulty in the questionnaire.

If all of the four conditions are satisfied, check the following path conditions and their corresponding packages. If all of them are correct, the transformation is written correctly.

Assuming the tester selects an interactive mode (Figure 7-1), first the tester is asked to specify whether an instance of in-pattern of the rule exists (Figure 7-2). Moreover, in the event that rules consist of a guard or conditions which their satisfiability cannot be inferred, the tester specifies if they are satisfiable (Figure 7-3). For the convenience of the tester, instead of the self keyword in the transformation definition, its related class namely Member is written in the wizard.

The result involves the time of symbolic execution, the satisfiable path condition, and its corresponding test model. The satisfiable path condition is also stored as a text file. Furthermore, the SMF is generated. The tester can click on Finish and investigate the SMF such that the final correctness of the ETL transformation is specified. It is also possible that the tester clicks on "Evaluate More" and inputs the expected SMF (Figure 8) and the tool specifies that whether the transformation written correctly (Figure 9).