-Model transformation is a key technology in modeldriven engineering. Unfortunately, transformations are typically written manually and thus they are likely to contain errors and to produce incorrect or undesired output. Safe transformation is the guarantee that for every possible source model, the transformed target model is valid with respect to user-definable wellformedness criteria. This paper introduces safe transformation for constraint-driven modeling (CDM), an approach that employs model transformation to generate target model constraints instead of generating a target model directly. Safe transformation for CDM ensures that transformations only produce correct and non-contradictory constraints. We demonstrate the feasibility of safe transformation and present a formal framework for applying it to CDM in arbitrary domains.
With the increasing popularity of Model-Driven Engineering (MDE) and modeling languages such as the Unified Modeling Language (UML), there is also an increasing need for validating the correctness of design models as they are used for safety-critical systems or other systems that are subject to strong regulations [1]. This verification consists of checking whether a model is syntactically and semantically correct. The desired conditions are usually expressed in form of model constraints, using constraint languages such as the Object Constraint Language (OCL).To date, there exist efficient approaches for checking constraints (e.g., [2]) on design models. However, these approaches are not readily applicable to model transformations [3] where both the source model and the target model must adhere to defined syntactic and semantic constraints. Of course, it is possible to verify a target model once it has been generated. However, what if we want to ensure that all generated target models are correct? The dilemma is that there are likely infinite possible source models and thus it is unscalable to generate all possible target models and verify them.
Safe model transformation ensures that transformations always produce results that meet defined criteria. These criteria are typically defined by designers based on either a specific metamodel or domain knowledge. For example, an important criterion may be that every transformation result is syntactically and semantically correct with respect to the target metamodel – i.e., the transformation will not generate an illformed target model. This implies that the applied criteria are likely to differ for different metamodels and domains. Safe model transformation is thus a warranty the transformation designer would like to provide to the transformation user (software engineer) – that the transformation result will always be correct with respect to the defined criteria, regardless of the given input model.
This work demonstrates safe transformation on Constraintdriven Modeling (CDM) [4]. CDM avoids premature design decisions by constraining target models instead of generating them directly. CDM uses model transformations to automate the generation of model constraints and to perform required updates. Hence, designers only have to write and maintain transformation rules instead of managing specific model constraints. However, transformation rules in CDM—and most other MDE-approaches—are written manually. This means that there is always a chance that these rules contain errors. CDM thus benefits from safe transformation as much as any other transformation-based approach would. Since CDM transforms source models into constraints, an incorrect transformation may result in contradictory constraints which make the problem of finding a valid model unsatisfiable. As an example, imagine two constraints forcing a model element to have two different values at the same time. Safe transformation for CDM ensures that defined transformation rules for a given source metamodel will never lead to contradictory constraints. This is a satisfiability test for which we apply the formal modeling and reasoning engine FORMULA [5]. Safe transformation generally ensures that all possible target models meet structural and static semantical conformance criteria [6]. For CDM, for instance, it ensures that no unsatisfiable constraints can be generated.
In this paper we present a formal approach for safe model transformation. The approach is generic and validates the correctness of arbitrary transformations on arbitrary metamodels and models by using a formal reasoning engine for automatic solution space exploration and transformation effect analysis. The approach uses only validity conditions and transformation definitions to automatically find input models suitable for validating transformation correctness. The feasibility and applicability are demonstrated in the context of constraintdriven modeling using the FORMULA [7] reasoning engine. For enabling reasoning about constraints as the result of model transformations, we used a formal (meta)modeling framework and formalized a basic consistency checking technique. In addition to a theoretical foundation, we validated the correctness of the implementation through systematic testing and by (a) (b) (c)
As a running example, we use an excerpt of a metamodel not unlike the UML metamodel as depicted in Fig. 1(a). The metamodel consists of the following elements: InstanceSpecification, Message, Class, Method, and ADClass. The element Class is used for modeling types. Such classes must provide a description, may have an arbitrary number of Method assigned, and may be part of a hierarchy if they have supertypes assigned (super). The element ADClass is a specialization of Class and provides an additional description, hence the prefix ”AD” and an array of size 2 for the field description. The element InstanceSpecification is used for modeling specific instances of modeled classes and Message elements are used for modeling method calls between instance specifications.
We use this metamodel to build the models shown in Fig. 1(b) and Fig. 1(c). In Fig. 1(b) a sequence diagram is shown that defines instance specifications a and b of the types A and B, respectively. Fig. 1(c) shows a class diagram in which the types A, B, and S are defined. A is a Class, B and S are instance of ADClass. S is also defined as superclass of B. The message named m, sent from a to b and highlighted by the rounded frame in Fig. 1(b), is added to the model. According to UML semantics, this means that the class B must provide a method named m. At first sight, a simple model transformation that automatically adds a method with the appropriate name to the defining type of the message receiver would solve the problem. Note, however, that adding a method to any of B’s superclasses and interfaces (e.g., S) would also be a valid option. Clearly, deciding where to add the required method – if a new method is required at all – is non-trivial and requires knowledge of the modeled system. Thus automating such a decision through a model transformation can be dangerous as it might produce undesired models. In the next section we will discuss how the constraint-driven modeling approach addresses this issue and also illustrate why safe transformation is important when transformations are used.
As the illustration shows, using model transformation in situations where more than one valid solution may exist is not straightforward and deciding which solution is correct involves domain knowledge that often cannot be generalized.
Using constraints avoids ambiguous transformations that may
produce invalid results. However, managing them manually
is non-practical in large models. The CDM approach tackles
this problem and uses transformations that generate constraints
on a model automatically instead of directly generating or
changing model elements. When using a traditional
transformation, the target model is generated or adapted automatically
through the transformation execution on the source model. In
contrast, the constraint-driven modeling approach executes the
transformation Tc on the source model SM to generate the
constraints C, as shown in Eq. (
The core idea is that defining invariants and desired conditions of valid models through constraints requires less knowledge and is therefore easier than defining a fixed set of rules that always produce a specific result that is always correct, (e.g., it is easier to define that two model elements must not have the same name than defining a rule that assigns meaningful names to all elements automatically). Moreover, constraints for similar elements (e.g., different instances of the same metamodel element) typically require similar constraints in which only specific parts differ, hence transformation rules can be seen as a structural template for a specific kind of constraint that can be instantiated and filled with data for specific model elements. Note that the target model TMc (the subscript c indicates that it is constrained) is not manipulated directly in our approach, neither through a transformation nor through constraints.
SM
T!c C
TMc
(
B must provide a method m (based on the message from a to b).
A must provide a description (based on its type
Class).
1We omit other invariants (e.g., that instances of Class and ADClass must provide a name) for space reasons. 11 1 r u l e RuleM
from s : Message 3 to t : C o n s t r a i n t (
e l e m e n t < s.receiver.type 5 i n v < ” s e l f . providedMethods >
e x i s t s (mjm. name = ’ ” + s.name + ” ’ ) ” ) 7 r u l e RuleC
from s : C l a s s 9 to t : C o n s t r a i n t ( e l e m e n t < s i n v < ” s e l f . d e s c r i p t i o n >s i z e ( ) =1 ” ) 13 15 r u l e RuleADC from s : ADClass to t : C o n s t r a i n t ( e l e m e n t < s i n v < ” s e l f . d e s c r i p t i o n >s i z e ( ) =2 ” ) Listing 1. ATL-like transformation rules to generate constraints.
S and B must provide two description fields (based on their type ADClass).
These requirements can be easily stated as constraints, for example written in OCL. To generate them automatically, we use ATL [8] to define the three transformation rules shown in Listing 1. The first rule RuleM (lines 1–6) is defined for messages in the model and creates constraints that require the receiver element’s defining class to provide a corresponding method. Note that this does not require the class to directly provide the method; it is sufficient that the method is defined somewhere in the class hierarchy (e.g., in a superclass).
Rule RuleC (lines 7–11) is executed for Class instances and generates constraints that check the cardinality of the attribute description. Finally, the third rule RuleADC (lines 12–16) checks that instances of ADClass provide two descriptions. Note that for simplicity we treat the two diagrams shown in Fig. 1(b) and Fig. 1(c) as one model (SM). When executing the transformation rules on the model in Fig. 1 we expect the following constraints to be generated:
C1 element B: self.providedMethods->exists(m| m.name=’m’) element A: self.description->size()=1 element B: self.description->size()=2 element S: self.description->size()=2 only produce the discussed constraints C1–C4, but – because instances of ADClass are also instances of Class – they will also create the following constraints C5–C6:
C5 element B: self.description->size()=1
C6 element S: self.description->size()=1 Obviously, the constraint combinations C3 ^ C5 and C4 ^ C6 are overconstraining the elements B and S, respectively. Both elements B and S are forced to have two different numbers of descriptions at the same time. Hence, the transformation leads to contradictory constraints.
The reason for this, somehow unexpected, result is that the transformation rules for cardinality checking constraints are defined for instances of the types Class and ADClass (lines 7 and 12 in Listing 1). Because ADClass is a subclass of Class, as defined in the metamodel depicted in Fig. 1(a), RuleC is also executed for all instances of ADClass. Indeed, the transformation rules RuleC and RuleADC need additional guarding statements that ensure the execution of only one of the rules per element. In fact, automating constraint generation may even increase the risk of contradictions between constraints and overconstraining of models as designers specify transformation rules that are executed when certain requirements are fulfilled. This means that – in contrast to manual addition of constraints to individual model elements – the aggregation of constraints restricting a model element is no longer directly visible for a designer. Note that this situation is not unique to constraint transformations. Such issues may arise in other domains as well. Using transformations to generate target models implies that the generated model is not known before rule execution. Automating model generation typically involves large numbers of transformation rules that are written for complex metamodels. Visualization of dependencies between these rules is usually not available and thus the risk of overlooking possible side-effects increases with the number of rules. Checking the correctness of transformation rules by looking at the results for existing sample models is not a valid solution to this problem as source models may change and thus cause errors in target models. This can also occur later during model refactoring, updates, or extensions when target models have to be re-generated. Next, we present how safe transformation helps designers avoid errors in target models.
C2 C3
C4 We expect one constraint to be generated for the message m and three constraints to be generated for checking the description attributes of Class and ADClass instances. The constraint C1 will show the inconsistency in our running example that b provides no method m. IV. SAFE MODEL TRANSFORMATION
Although the constraints in such a small example could be As we have shown in the previous section, writing transwritten manually, maintaining a large number of constraints formation rules – regardless of the specific domain – can be a during the modeling process where the metamodels and mod- highly complex task as there may be source models that cause els change frequently is error prone. Consequently, constraints the execution of combinations of rules that are not supposed should be managed automatically. We have shown that CDM to be executed together or also the execution of rules for is practical in [4]. elements where the rule should not be executed at all. Safe
However, even with automated constraint management, model transformation guarantees that a transformation designers manually write transformation rules or templates will always produce valid results. Validity rules are defined for desired constraints that can be executed or instantiated, by designers and typically stem from both the metamodel of respectively. Thus there is no guarantee that these transforma- the transformation’s target model (syntax rules) and domain tion rules or templates produce constraints that are syntacti- knowledge (semantic rules). Intuitively, safe transformation cally and semantically correct. Coming back to our running can be easily proven for a single source model by executing example, the transformation rules in Listing 1 actually not the transformation and validating whether the target model is valid with a SAT-solver. However, our definition of safe transformation is that a transformation must not, under any circumstances, produce invalid results, meaning that there must not be any possible source model that causes invalid results.
Based on the conventional notation for model transformation,
we can formally define a transformation as the function shown
in Eq. (
Saf e(SMM; T ) , 8sm trans : (sm validS : sm validT : tm
SMM; T ) ! tm
TMM
SMM : validS (sm)
SMM : validS (sm)^
) validT (trans(sm; T ))
:validT (trans(sm; T ))
(
The FORMULA reasoning engine supports automatic proofs through solution space exploration and transformations, thus it is an ideal choice for implementing safe transformation. However, any reasoning engine for automatic proofs can be used in principle, even though this could require the additional formalization of transformations. The solver is capable of expanding models on its own for finding proofs and partial models can be used for reasoning. For details about the reasoning mechanism please refer to [7] and [5].
Note also that safe transformation does not rely on static analysis and thus allows arbitrary input/output (meta)models, transformation languages, and conditions. The approach therefore is generic and not limited to specific domains or languages. Moreover, the complete integration of input model construction, the transformation, and the validity conditions means that both the validity conditions and the transformation itself are available to the solver for reasoning, potentionally enabling higher efficiency and precision.
b to indicate that a is an instance of b.
V. APPLYING SAFE MODEL TRANSFORMATION TO
CONSTRAINT-DRIVEN MODELING
As discussed in Section III, constraints can be contradicting. Because we need to formally specify such a contradiction in order to apply safe transformation, let us first give formal definitions of constraints and the models they are applied to.
Constraints restrict model elements, therefore we need a
formal definition of metamodels and models along with
constraints definitions. Eq. (
MMcdm := hT ypes; CExpri
(
M Mcdm := hN; E; Cij N = fxjx
y 2 T ypesg^ E = fha; b; cija 2 N ^ b 2 N ^ c N g^
C = fhcontext; expijcontext 2 N ^ exp value : (N; N ) ! P(N ); (x; y) 7! z : 9hx; y; zi 2 E validate(c 2 C) 7! (inconsistent if c is violated
consistent otherwise allowed(ha; b; ci
n 2 a ^ e 2 a ^ v a ^ r c^ (9hh; i; ji 2 E : n = h ^ e = i)^ (y = value(n; e) ^ y 2= v ) 9rx 2 r : validate(rx) = inconsistent)g contradiction(m
M Mcdm) , 9hn; e; v; xi 2 allowed(m) :v = ;
(
We define the generic constraint validation function as
shown in Eq. (
Now that the metamodel and the corresponding functions for constraint validation and the detection of contradictions are defined, we can use this information to check the transformations from Section III.
We converted the ATL-like transformations shown in Listing
1 to transformations Tcdm that can be executed by the
FORMULA solver. A constraint transformation CT can be written
as shown in Eq. (13). When executing the transformation for
a source model sm MMcdm, the result is the constrained
model tmc MMcdm which includes all model elements
defined in sm and a set of constraints generated for these
element. The last part needed for safe transformation are the
source and target validity functions validScdm and validT cdm,
respectively. For the former, the conditions are domain-specific
and thus independent of CDM. Therefore, we omit a formal
definition in Eq. 14. For the latter, results to be valid if they
are free of contradicting constraints, as shown in Eq. (15).
By substituting the constraint transformation function (13), the
metamodel definition (
CT : sm
MMcdm
Tcdm! tm
MMcdm validScdm(x
MMcdm) , x is syntactically correct
and valid w.r.t. domain semantics validT cdm(x
(13) (14) (15) (16)
MMcmd : validScdm(sm) ^ :validT cdm(CT (sm)) Note that we use the transformation function CT directly on the right-hand side of the equation and thus we eliminate the corresponding argument on the left-hand side. We now ask the FORMULA solver to prove this condition and search for examples of source models sm that lead to invalid target models: solve CT sm Unsafe. The solver will return an input that leads to a contradiction, which tells us that the transformation is unsafe. In particular, this input will include an instance of ADClass and also include facts that help designers find the constraints and the transformations that caused the contradiction).
Assume that, after taking a closer look at the transformation rules RuleC and RuleADC based on the solver output, we identified the error and added guarding statements (e.g., s.getClass().getName()="Class") so that RuleC is no longer executed for instances of ADClass. Asking the solver again for an example sm of a contradiction-causing model will fail and the solver will tell us that it could not find such an example, meaning that the transformation is safe.
In addition to the presented theories, we demonstrate the applicability of the generic safe transformation approach by implementing it for constraint-driven modeling. We also discuss threats to validity in this section.
In the paper we presented the theoretical foundations of safe model transformation. The presented conditions are correct and they capture the ideas and principles of safe transformation. The correctness was further assessed by implementing those conditions and functions in a program that produced correct results as we discuss next.
To ensure the feasibility of safe transformation and the validity of the theoretical foundations presented in the paper, we have implemented a safe transformation framework for CDM using the FORMULA language. This implementation is a straight forward translation of the presented formal definitions to type declarations and functions, thus we omit a detailed discussion. It allows the definition of metamodels and models (based on an existing metamodeling framework [5]), and it supports the definition of constraints. Moreover, it provides functions for constraint evaluation and for reasoning about constraints. For this feasibility study we used a subset of the constraint expressions available in OCL. The correct behavior of the implementation was ensured through testing with systematically varied inputs for expressions.
As mentioned in Section V, we used the implementation with the model discussed in Section II and the transformation rules from Listing 1. For the running example and the incorrect transformation rules, the FORMULA solver returned different solutions (i.e., sample models) that all included an instance of ADClass and contained contradicting constraints. Moreover, the resulting facts derived by FORMULA included as many constraint contradictions as there were ADClass instances. After fixing the transformation rules, the problem was not satisfiable anymore – as expected. This indicates that the translation to FORMULA is correct and the approach produces the desired result in practice.
The presented framework is suitable for ensuring safe transformation for CDM in arbitrary modeling domains. To enable safe transformation in general (i.e., for transformations different to those used in CDM), the following three steps are necessary: i) define source and target metamodels using an existing metamodeling framework, ii) describe transformation rules in FORMULA, and iii) describe desired validity conditions. We believe that the metamodel definition can be automated for metamodels based on common frameworks (e.g., MOF). The transformation description in FORMULA is straightforward and uses concepts similar to common transformation languages such as ATL – this step may also be automated. Overall, we deem the effort needed for using safe transformation acceptable given the importance of transformation correctness and the effort required for locating and fixing errors caused by unsafe transformations in later development stages. Overall, we believe that the steps required for using the framework are manageable.
We have used the FORMULA solver for finding input models for which a transformation is unsafe with respect to defined criteria. Indeed, FORMULA is capable of searching solutions efficiently. Nevertheless, it can only guarantee that there is no solution for a defined maximum size of solution models [5]. In [9], Sen et al. use Alloy for constructing test models that meet defined well-formedness criteria from partial models. We use this principle more extensively as our input data for constructing input models for transformations is often empty. Although we expect target model errors to typically involve only a relatively small number of elements, the bounded search space is a practical threat to validity. Even if current solvers might not find input models that unveil errors in transformations, manually written test models are far from finding all errors [9], thus our approach gives designers additional confidence in the correctness of their work.
Model transformation has become a very active field of research. We now discuss other approaches closest to our topic. Sen et al. [9], [10] presented techniques for finding input models for testing model transformations. They use Alloy to expand partial models automatically to complete models that conform to well-formedness rules. The fact that they use different languages and strategies for finding sample models shows that our generic approach can be implemented with a range of languages. Note, however, that safe transformation integrates the construction of test input models and the execution of transformations. Guerra et al. [11] propose the use of contract for validating transformation correctness. This is basically the same concept safe transformation uses. However, they use QVT to enforce defined pre- and post-conditions of transformations and rely on existing input models while safe transformation uses such contracts to actively search for input models that lead to a violation of the target model constraints. Cabot et al. [12] proposed an approach for deriving OCL constraints from declarative transformation specifications. Their approach generates invariants that must hold between source and target models. Our approach can be used to ensure that, for example, only non-contradicting invariants are generated. Jackson et al. [5] previously used FORMULA for describing a general purpose (meta)modeling framework.The reasoning they did about transformations based on their framework can be seen as an application of the safe transformation approach to identify undesired behavior of transformations.
In this paper we presented the safe transformation approach that allows the use of formal modeling languages for proving assumptions about arbitrary model transformations for either arbitrary source models or also source models with specific characteristics. In particular, we demonstrated its applicability for the constraint-driven modeling approach by ensuring constraint satisfiability and checking the semantical correctness of transformation rules and their results. The safe transformation approach was validated by implementing it using the FORMULA language. For future work we plan to integrate the framework in existing tools that use CDM and also implement the approach for other domains.