Query Structured Model Transformation (QueST) is a framework for de ning source-to-target Model Transformations (MTs) in a structured and declarative manner. In this paper, we study how MT-related properties can be analyzed in QueST. Each MT in QueST is equivalent to a logical theory and checking properties for the MT is equivalent to analyzing correctness of such properties (i.e., demonstrating that they are theorems) in this theory. We will explain the idea by encoding an underlying theory of a simple MT example as an Alloy speci cation and de ning three sample properties. We show that the correctness of one of the properties is refuted by the Alloy analyzer, and provide a manual proof for the other two.
1Here we follow the terminology developed in [ACL+14], which distinguishes language-related property checking, such as termination and determinism, vs. MT-related property checking that is speci c to each MT de nition.
can use a model checker or an instance generator like Alloy (for a limited scope analysis). If the logic used for encoding is complete, we can replace semantic validity by syntactic provability, T h(D) ` P , so the problem would be equivalent to proving or disproving the correctness of proposition P in the theory T h(D). This process can be performed manually, or by receiving some assistance from a theorem prover.
The very idea of logical encoding of MTs for property checking is not new [BECG12, CLST11]. However, two features of QueST make it very well suited for the realization of this idea. First, an MT de nition in QueST is itself close to its logical encoding as a theory: we can see a query language as an algebraic version of the corresponding logic. For example, the well-known equivalence of relational algebra and rst-order logic means that any relational query can be reformulated as a FOL formula. Second, QueST's MT de nitions are amenable to being built in a structured and modular way [GDM14], and their structural properties are directly transformed to their logical encoding.
analyses. Note, however, that QueST's MT analysis method is independent of the implementation tool like Alloy.
and explain how MTs are de ned in QueST. In Section 3, we present a logical encoding of the example in the
2
2.1
who drive vehicles. The source and the target metamodels are depicted with light gray squares in Fig. 1 (the target metamodel on the right and the source metamodel on the left). Boxes and arrows in the metamodels denote classes and associations, and red bracketed expressions indicate constraints (ignore the green dashed elements for the moment). There are two requirements for the translation. The rst is that cars and vehicles are considered to be synonyms: every car in a source instance should be a vehicle in the target, and conversely.
Source!Metamodel! likes$[*]$ Person$ [1..*]$ [*]$ owns$ QisA$
Qboth$
Qdrive! QPerson$
Car$ map2$ map3$ map1$
! View!
! Mapping! !
Target!Metamodel! HappyPerson$ Vehicle$
[*]$ drives$
by the target metamodel: each element (a class or an association) in the target metamodel is to be mapped to a corresponding element (class or association, respectively) in the source metamodel. For example, class Vehicle is mapped to class Car (see Fig. 1) because they should be isomorphic, given the requirements of the MT.
the association drives, and the QueST idea is to reproduce such \missing" elements by nding suitable queries against the source metamodel, which result in exactly the elements needed to complete the mapping. Thus, for the HappyPeople MT, we need to nd queries against the source metamodel, which would derive a class and an association corresponding to the class HappyPerson and the association drives in the target metamodel. We build such queries in two steps described below as queries Q1 and Q2.
To ease understanding of our query descriptions, we switch to the terminology of relational theory, in which classes and associations are referred to by their intended semantic interpretation as sets and (binary) relations, respectively.
the precise semantics of the above queries in Alloy.
After the source metamodel is extended with required derived elements, we can complete the MT de nition mapping as shown in Fig. 1 (we also call it the view mapping, as what such a mapping de nes is exactly a view whose schema is given by the target metamodel). The mapping is shown as a block arrow comprising three individual links that we call maps: map1 , map2 , map3 . Syntactically, the mapping is a graph morphism from the target metamodel graph to the augmented source metamodel graph. Semantically, the mapping comprises a set of bijections between the elements in the target and the source metamodels. At the time of MT execution, the three map arrows specify how the elements of a speci c type are generated in the target. For example, (a) Input Source model
(b) Generated target model all the elements of HappyPerson in the target are generated from the elements of QPerson produced by the corresponding query.
Fig. 2(a) is a source model, and Fig. 2(b) is its corresponding target model generated by the above QueST MT de nition1. Indeed, as each of Person1 and Person2 owns and likes the same car (i.e., Person1 owns and likes Car1 and Car2, and Person2 owns and likes Car0 ), they appear as happy people in the target model. The cars they both own and like also appear in the target as vehicles they drive. A general speci cation of the QueST execution mechanism can be found in [Dis09, GDM14]. 3
concrete language, say SQL, or OCL. In addition, we need a language to encode the view de nition mapping. Both, the mapping and queries (operations) can be encoded with constraints. For example, to encode a binary operation, we introduce a ternary predicate R with a constraint that for any x and y, there is one and only one z such that R(x; y; z) holds true. Encoding of mappings will be explained below. Thus, as soon as we have a su ciently expressive logical language L (e.g., FOL, OCL, or another appropriate alternative), an MT de nition in QueST can be encoded as a theory in L. In this section, we show how the HappyPeople MT can be presented as an Alloy speci cation; i.e., we use Alloy as L. Then we present encoding of properties in Alloy, and show how we can check them. 3.1
Alloy enables quick development of speci cations and provides facilities for their analysis [Jac12]. Alloy's primary concepts are sets and (binary) relations, so that any system is modelled as a collection of sets and relations with a number of constraints de ned over them. Relations are understood both extensionally (as sets of ordered pairs, R A B) and navigationally (as partial multi-valued mappings, R : A 9 B; below we will use stroked arrows for relations and ordinary arrows f : A ! B for functions, i.e., single-valued relations). The major operations of the extensional view are ordinary set union, intersection and complement. The major operation of the navigational view is relation composition: relations R1 : A 9 B and R2 : B 9 C can be composed into R1:R2 : A 9 C with the following semantics: 8a : A; 8c : C; (a; c) 2 R1:R2 () 9b : B; (a; b) 2 R1 ^ (b; c) 2 R2.
1These instances are generated by the Alloy tool after encoding of the above QueST MT de nition in Alloy. We will discuss the encoding process in Sec. 3.1.
constraint or query can be speci ed in several di erent ways, providing great exibility in using the language.
In the following, we explain how we encode di erent components of a typical QueST MT including metamodels, queries and mappings, and combine them in a uni ed Alloy speci cation. Because of the Alloy speci c syntax for specifying relations, it is not possible to completely separate the encoding of these components in the syntax; however, by adding comments inside the speci cation we will provide a distinctive view representing each component encoding. //map1 bijection[map1,HappyPerson,QPerson] //map2 bijection[map2,Vehicle,Car] //commutivity constraints ensuring map3 (see Lemma 1) drives.map2=map1.Qdrives
in QueST. Therefore, the source and the target metamodels of an MT can be directly encoded in Alloy. In Fig. 3, lines 3,5 and 6 encode the source metamodel (see Fig. 1), and lines 9 and 11 encode the target metamodel. Classes become signatures, and associations become relations de ned inside curly brackets of their corresponding domain signature; e.g., likes : P erson 9 Car and owns : P erson 9 V ehicle are two relations de ned under signature
the query. The Relation Intersection Query produces the relation Qboth (see line 4), and the Domain Restriction Query produces the set QPerson and the relation Qdrives (see line 29). The QisA relation in Fig. 1 is encoded implicitly by the in keyword at line 29, denoting the subsetting relation between QPerson and Person. The semantics of the query operations are re ected as constraints over the query results. For the Intersection Query, line 26 ensures straightforward intersection semantics for Qboth. Lines 30-31 specify the corresponding constraints for the Domain Restriction Query results. QPerson = Qboth:univ at line 30 makes QPerson equal to projection of Qboth onto Person, and Qdrives = Qboth at line 31 is in fact a concise encoding of Qdrives = QisA Qboth, since QisA is an identity relation. 3.1.4
In the HappyPeople example, the view mapping consists of three mapping links or just maps connecting the target metamodel with the source metamodel. Semantically, if a map links two classes, (like map1 and map2 ), then it speci es a bijection between the corresponding sets, and we add to our Alloy speci cation the corresponding facts (see lines 16-19). If a map links relations like map3, semantically it means a bijection between the relations as sets of pairs, and moreover, the following commutativity constraint: if map3(h; v) = (p; c), then map1(h) = p and map2(v) = c. However, Alloy does not allow us to de ne a relation between relations like map3 , and we need to nd a work-around.
Lemma 1. Let Ri : Ai 9 Bi, i = 1; 2 be two relations, and f : A1 ! A2, g : B1 ! B2 two functions such that the following commutativity condition holds: R1:g = f:R2. Then there is a uniquely de ned function f g : R1 ! R2 between relations as sets such that for a pair (a; b) 2 R1, f g(a; b) = (f (a); g(b)). Moreover, if functions f; g are bijections, function f g is a bijection as well (and in this case we say that relations R1 and R2 are isomorphic).
3.2
that let us use the Alloy analyzer to check their validity. The Alloy analyzer works based on scope parameters; that is, assertions are checked within a user-de ned scope that limits the maximum number of elements of each set. In the case that Alloy nds a counterexample within the de ned scope, it means the assertion is not valid; otherwise, the assertion is valid within the scope, but might be valid beyond it.
did nd a counterexample for the second assertion refuting its correctness: there might be some vehicles without a driver in the generated models. Fig. 5 demonstrates one of these counterexamples generated by the Alloy analyzer. In the gure, the source model (gray elements), the generated model (blue elements), query results (green elements), and the traceability links (red arrows labeled with map1 and map2 ) are all presented explicitly.
Vehicle1 in the generated model that comes from Car1 is not driven by anybody. } // P r o p 2 : all v e h i c l e s are d r i v e n by s o m e b o d y a s s e r t ass2 {
all v : V e h i c l e | some h : H a p p y P e r s o n | h - > v in d r i v e s } // P r o p 3 : if s o m e b o d y d r i v e s a v e h i c l e he l i k e s that v e h i c l e a s s e r t ass3 { all h : H a p p y P e r s o n | all
v : V e h i c l e | h - > v in d r i v e s = > map1 [ h ] - > map2 [ v ] in l i k e s
For the rst and the third property, Alloy could not nd any counterexamples, meaning that they might be valid even for an unlimited scope. One way to increase certainty about their validity is to increase the scope parameter value to a higher number; but no matter how much we increase the scope boundaries, the uncertainty will never disappear. To gain greater con dence, we need to provide a formal proof (which gives us absolute con dence modulo the adequacy of the formal encoding of the subject matter). This could be done manually, or semi-automatically with a theorem prover, but in general provability of FOL statements is undecidable; the latter of course does not prevent the existence of decision procedures for speci c fragments and cases.
Lemma 2. Two isomorphic relations (see Lemma 1) have the same head and tail multiplicities.
Theorem 1 (Property 1 Holds). Every happy person drives at least one vehicle, formally: (8h:HappyPerson; 9v:Vehicle)v 2 h:drives.
T h j=
Theorem 2 (Property 3 Holds). If a happy person drives a vehicle, this person likes the corresponding car in the source model. Formally, T h j= (8h:HappyPerson; 8v:Vehicle)v2h:drives ) map2 (v)2map1 (h):likes
Qdrives: T h j= c2p:Qdrives ) c2p:likes for all p2QPerson, c2Car (recall that QPerson is a subset of Person). Now it is easy to see that the property above means that Qdrives likes, which is obvious as Qdrives=Qboth and Qboth=owns \ likes likes.
maps the target metamodel M MT into a suitable extension of the source metamodel with derived element, Q(M MS ), where Q refers to a set of queries providing the extension. When we need to prove a property that involves target metamodel elements (which is a typical case), we replace those elements by their images in Q(M MS ) and rewrite the property accordingly (an accurate formal speci cation of this construction can be found in [DW08]). The problem thus amounts to property analysis over Q(M MS ), which is a standard logical problem studied in databases: given a relational schema with constraints, M MS , analyze the properties of the queries Q(M MS ) against the schema. We plan to investigate how the results obtained by the database community can be adapted for MT in our future work. 4
Paper [ACL+14] provides a useful classi cation of model transformation techniques. In their terminology, our present work lies in the Type 2 category which classi es Transformation Dependent and Input Independent veri cation techniques. More speci cally, Formulating the MT as a theory is similar to theorem proving techniques. Calegari et. al. work [CLST11] is the closest to our work in this category. They presented encoding of ATL transformation as a logical theory in Coq: metamodels are translated to inductive types and model transformation rules to logical formulas, and properties speci ed as propositions in the corresponding theory; then they used Coq theorem prover to analyze the properties. The main di erence of our work with [CLST11] originates from the di erences in transformation components (i.e., ATL rules vs. QueST queries) which e ects the shape of axioms in the theory. We brie y discussed the di erence of QueST with a rule based MT language in [GDM14] from engineering perspective.
speci cation. The authors of paper [BECG12] provide an automatic translation of ATL transformations to transformation models expressed as an OCL theory, and used OCL model nder to analyze the properties. This is similar to encoding of an MT in Alloy and using instance nder to check their properties. In [MC13], the authors used Alloy to encode QVT-R transformations and proposed an alternative enforcement semantics for that. Papers [CGR13, MRR11] proposed a translation between the UML class diagram and Alloy for the validation and veri cation of class diagrams. The authors in [ABK07] translate source and target metamodel to alloy and specify the transformation rules as mapping relations. In [GK15], the authors introduce a sub-language of Alloy called F-Alloy that is used for expressing a functional mapping representing a transformation. Similar to [CLST11], papers [ABK07, GK15] follow the common MT paradigm that a source-to-target transformation is speci ed as a set of mappings going from the source to the target elements, whereas in QueST these mappings go in the opposite direction. Finally, authors in [SLC+14] employed a di erent technique based on symbolic execution for graph-based MT veri cations. 5
in the QueST framework: every transformation de nition in QueST amounts to its corresponding theory, and checking properties is equivalent to proving or disproving the corresponding theorems in this theory. Using a simple MT example, we demonstrated how the latter mechanism works: we encoded the theory of the example in Alloy, and used its analysis facilities to disprove a sample property. Then we provided manual mathematical proofs for the other two properties.
work [GDM14] that QueST is applicable to larger and more complex examples like the transformation of Class
proofs of the properties to be checked, but the proposed approach to the veri cation would still be valid and applicable. As a future work, we plan to apply the proposed method to a large-scale industrial application and further study how the structured nature of QueST's speci cation of MTs might be helpful in managing the complexity of property checking. [ABK07]