One hinderance to model transformation verification is the large number of different MT languages which exist, resulting in a large number of different language-specific analysis tools. As an alternative, we define a single analysis process which can, in principle, analyse specifications in several different transformation languages, by making use of a common intermediate representation to express the semantics of transformations in any of these languages. Some analyses can be performed directly on the intermediate representation, and further semantic models in specific verification formalisms can be derived from it. We illustrate the approach by applying it to ATL.
A large number of different transformation languages exist, ranging from
declarative languages such as QVT-R [
In this paper we describe a general language-independent framework for transformation verification, and describe a range of language-independent verification techniques. The framework is based upon metamodels which provide language-independent representation of transformation specifications (Section 2). These representations can then be mapped via semantic mappings to suitable formalisms which support verification (such as theorem provers or constraint satisfaction checkers). This approach means that only one semantic mapping needs to be defined and verified for each target formalism, rather than semantic maps for each different transformation language and target formalism.
Transformations operate on various models or texts which conform to some metamodel/language. There may be several input (source) models used by a transformation, and possibly several output (target) models. A transformation is termed update-in-place if a model is both an input and output, otherwise it is a separate-models transformation. Languages can be specified in many different ways, e.g., by UML class diagrams, by BNF syntax definitions, etc. Here we will use UML class diagrams, together with OCL constraints. These form the concrete syntax of language descriptions.
Figure 1 shows a generic metamodel (termed LMM) which can serve directly or indirectly as a metamodel (abstract syntax) for a wide range of modelling languages. The metamodel is also self-representative. EntityType represents classes and interfaces, DataFeature represents both attributes and associations. mult 1lower and mult 1upper refer to the multiplicity range of the source side of the attribute/association (i.e., the side with the entity type which owns the data feature), whilst mult 2lower and mult 2upper refer to the multiplicity range of the target side (the side with the type entity type). A value of −1 for an upper bound indicates a *-multiplicity at that end. isOrdered refers to the ordering of the target end.
A metaclass Language representing languages has a set entityTypes of EntityType,
a set features of DataFeature, and a set constraints of Constraint . Many
variations on constraint languages could be used, here we adopt the subset of OCL
2.3 used in UML-RSDS [
An optional association end (with mult 2lower = 0 and mult 2upper = 1) is formally represented as a set (or sequence) of size 0 or 1. A denumerable type Object OBJ is included in each LL to represent the set of all possible object references. A finite set objects ⊆ Object OBJ represents the set of all existing objects at any point in time. Each entity type E has E ⊆ objects. Constraints in the expression language Exp(L) are mathematically represented as first-order set theory axioms in LL, for each base language L.
At the specification level, the effect of a transformation can be characterised
by a collection of mapping specifications, which relate model elements of one or
more models involved in the transformation to each other [
In this figure, Mapping , TransformationSpeci cation, ModelEnd , and MappingEnd
are subclasses of NamedElement . Each mapping has a corresponding
computation step which defines the application of the mapping to specific source elements
that satisfy its condition. Transformation specifications in declarative
transformation languages can be expressed in this metamodel, using abstraction
techniques such as those defined for TGG (triple graph grammars) and QVT-R in
[
The rules:relation constraints express the postconditions Post of the transformation. Typically each mapping relation constraint Cn ∈ Post has the form of an implication SCond implies Succ forall-quantified over elements (the source mapping ends s : Si ) of the source models. The assumptions express the preconditions Asm of the transformation. The invariants define properties Inv which should be true initially, and which should be preserved by each computation step of the transformation. 3
The following verification techniques can be applied to the T MM representation
of transformations, as follows:
{ Syntactic analysis to identify the definedness conditions def (Cn) and
determinacy conditions det (Cn) of each mapping constraint Cn. These are
the conditions necessary for Cn to have a defined and determinate value,
respectively [
Figure 3 shows an example of data dependency analysis being performed on the T MM representation of an ATL specification: two rules are identified as writing to the same entity type and feature, so are potentially in conflict. 4
} ... rule rn { ... } the T MM representation of M is a transformation specification M ′, and each matched rule ri is represented by two mappings ri Matching and ri Initialisation of M ′, which both have readOnly mapping ends the sj : Sj . The tk : Tk are created mapping ends of ri Matching , and updated ends of ri Initialisation. The input conditions SCond are translated to a condition conjunct SCond ′ of ri Matching and ri Initialisation. Any using variables are expressed by a conjunct vt = valt ′ of the condition. The output variables become exists-quantified variables of the relations of the ri mappings. If an action block Stat is specified, then a new update operation opri (s2 : S 2; :::; sm : Sm; t 1 : T 1; :::; tk : Tk ) is introduced, this operation has activity given by the interpretation Stat ′ of Stat as a UML activity. The resulting relation of ri Matching has context S 1 and predicate
T 1→exists(t 1 | t 1:$id = $id ) and ::: and Tk →exists(tk | tk :$id = $id ) This creates target model elements corresponding to the source model elements that satisfy SCond ′, and establishes tracing relations from s1 to t 1, ..., tk by assignment of an identifier attribute $id , which is added to each root class of the source or target metamodels. The relation of ri Initialisation has context S 1 and predicate
T 1→exists(t 1 | t 1:$id = $id and ::: and
Tk →exists (tk | tk :$id = $id and TCond 1′ and ::: and TCondk ′ and
s1:opri (s2; :::; tk )):::)
In this rule the previously created tj corresponding to s1 are looked-up and their
features initialised. Lazy rules r with first input entity type S 1 are translated to
operations rop of S 1. Calls thisModule:r (v 1; :::; vm) to the rule are interpreted
as calls v 1:rop(v 2; :::; vm) of this operation. The operation rop is stereotyped as
≪ cached ≫ in the case of unique lazy rules2. All ri Matching rules are listed
2 Iterative target patterns are not treated by this translation. These are a deprecated
feature of ATL since ATL 2.0.
before all the ri Initialisation rules in M ′:rules. The translation from ATL to
T MM can be extended to update-in-place transformations, i.e., to the re ning
mode of ATL (ATL 2010 version). The translation from ATL to T MM has
been implemented in the UML-RSDS tools [
The translated transformation in T MM represents the usual execution
semantics of the ATL transformation, in which target objects are created in a
first phase, followed by links between objects [
Using B, syntactic correctness can often be proved by using invariants of the transformation to relate the target model to the source model. Thus a proof of syntactic correctness of this kind also demonstrates syntactic correctness for the original transformation. Similarly, model-level semantic preservation can often be shown by invariant-based reasoning, which can be transferred from the translated specification to the original.
A counter-example produced by Z3 or another satisfaction-checking tool gives a pair (m; n) of a source and target model which can result from completed execution of the translated transformation, and where n violates some constraint of T . Such a pair is also a counter-example to syntactic correctness of the original ATL transformation. For refining mode transformations, termination and confluence of the translated specification establishes these properties of the original specification. 5
In this section we evaluate the approach by considering two example case studies:
the simple UML to relational database example from the ATL Zoo, and the
refactoring transformation of [
{ t.tcols->includes(thisModule.makePrimaryKeyColumn(att)); } } for ( att in c.ownedAttribute ) { if ( att.type.oclIsKindOf(Entity) )
{ t.tcols->includes(thisModule.makeForeignKeyColumn(att)); } } for ( att in c.ownedAttribute ) { if ( att.type.oclIsKindOf(PrimitiveType) or att.isPrimary = false ) } } } } } { t.tcols->includes(thisModule.makeColumn(att)); } } lazy rule makePrimaryKeyColumn { from p : Property ( p.isPrimary ) to c : Column ( rdbname <- p.name, type <- p.type.name ) lazy rule makeForeignKeyColumn { from p : Property ( p.type.oclIsKindOf(Entity) ) to c : Column ( rdbname <- p.name, type <- "String" ),
f : FKey ( references <- p.type, fcols <- Set{ c } ) } lazy rule makeColumn { from p : Property ( true ) to c : Column ( rdbname <- p.name, type <- p.type.name )
The matched rule is translated to two constraints C 0 and C 1 with context Entity: generalisation.size = 0 implies
Table->exists( t | t.$id = $id and t.rdbname = name ) generalisation.size = 0 implies
Table->exists( t | t.$id = $id and self.makeTable1op(t) ) C 1 has the condition and relation of makeTableMatching, and creates table objects and sets their attribute values. C 2 has the condition and relation of makeTableInitialisation, and looks up table objects using the introduced primary key $id and creates and links columns to the tables. makeTable1op(t ) carries out the procedural code of makeTable’s action block, invoking operations makePrimaryKeyColumnop, makeForeignKeyColumnop and makeColumnop of Property corresponding to the lazy rules. For example: makeColumnop(): Column post:
Column->exists( c | c.$id = $id and c.rdbname = name and c.type = type.name and result = c )
Figure 3 shows an example of data-dependency analysis on the translated specification. Verification properties of interest for this case study include: (i) termination; (ii) confluence (meaning that semantically equivalent source models are always mapped to equivalent target models); (iii) that the columns of the foreign keys are always contained in the set of columns of the tables, formalised as the transformation invariant fcols ⊆ Table:tcols on FKey.
For this specification (i) can be shown by data-dependency analysis, establishing that a bounded iteration implementation is sufficient for C 0 and C 1. (ii) fails because the association end Table :: tcols is ordered, so that different representations of the same input model may result in semantically distinct result models. Proof of (iii) can be carried out by establishing it as a transformation invariant in B. Table 3 shows the results of verification for the transformation. Atelier B version 4.0 was used.
The refactoring transformation of [
Since the transformation involves fixed-point iteration, termination is shown by proving that Property :allInstances()→size() is a variant, i.e., that the number of Property instances in the model is always strictly decreased by applying the transformation rule. Table 4 shows the results of verification for the transformation.
Property ATL via T MM Termination 6 proof obligations, 5 automatically proved Single inheritance 13 proof obligations, all automatically proved No name conflicts 15 proof obligations, 13 automatically proved
Table 4. Proof effort for refactoring transformation 6
In [
We have outlined a language-independent approach for model transformation verification, and illustrated this approach by applying it to ATL. We also intend to apply this approach to other hybrid MT languages, such as ETL, Flock, GrGen.NET and QVT-O.