Softw Syst Model (2010) 9:335–357
DOI 10.1007/s10270-009-0129-0
SPECIAL SECTION PAPER
A UML/OCL framework for the analysis of graph transformation
rules
Jordi Cabot · Robert Clarisó · Esther Guerra ·
Juan de Lara
Received: 6 November 2008 / Revised: 23 July 2009 / Accepted: 31 July 2009 / Published online: 19 August 2009
© Springer-Verlag 2009
Abstract In this paper we present an approach for the
analysis of graph transformation rules based on an intermedi-
ate OCL representation.We translate different rule semantics
into OCL, together with the properties of interest (like rule
applicability, conflicts or independence). The intermediate
representation serves three purposes: (1) it allows the seam-
less integration of graph transformation rules with the MOF
and OCL standards, and enables taking the meta-model and
its OCL constraints (i.e. well-formedness rules) into account
when verifying the correctness of the rules; (2) it permits
the interoperability of graph transformation concepts with a
number of standards-based model-driven development tools;
and (3) it makes available a plethora of OCL tools to actu-
ally perform the rule analysis. This approach is especially
useful to analyse the operational semantics of Domain Spe-
cific Visual Languages. We have automated these ideas by
providing designers with tools for the graphical specification
Communicated by Jeff Gray, Alfonso Pierantonio, and Antonio
Vallecillo.
J. Cabot (
B
) · R. Clarisó
Universitat Oberta de Catalunya, Barcelona, Spain
e-mail: jcabot@uoc.edu
R. Clarisó
e-mail: rclariso@uoc.edu
E. Guerra
Universidad Carlos III de Madrid, Madrid, Spain
e-mail: eguerra@inf.uc3m.es
J. de Lara
Universidad Autónoma de Madrid, Madrid, Spain
e-mail: Juan.deLara@uam.es
Present Address:
J. Cabot
Estudis d’Informàtica, Multimèdia i Telecomunicacions,
Rbla. del Poblenou 156, 08018 Barcelona, Spain
and analysis of graph transformation rules, including a back-
annotation mechanism that presents the analysis results in
terms of the original language notation.
Keywords Graph transformation · OCL ·
Meta-modelling · Domain Specific Visual Languages ·
Verification and validation
1 Introduction
Model-Driven Development [58] (MDD) is a software engi-
neering paradigm where models play a fundamental role.
They are used to specify, simulate, test, verify and gener-
ate code for the application to be built. Most of these activ-
ities are model manipulations, thus, model transformation
becomes a crucial activity. Many efforts have been spent
in designing specialized languages for model transforma-
tion, ranging from textual to visual; declarative to imperative
through hybrid; and semi-formal to formal. The OMG vision
of MDD is called Model-Driven Architecture (MDA) [38]
and is founded on standards like QVT [49] for transforma-
tions and MOF [43] and OCL [44] for modelling and meta-
modelling.
Graph Transformation [23,52] is a declarative, rule-based
technique for expressing model transformations. It has been
used for specifying in-place transformations like animations
[25], simulations [20], optimizations and redesigns [42]. It
is now gaining increasing popularity due to its visual form
(making rules intuitive) and formal nature (making rules and
grammars amenable to analysis). For example, it has been
used to describe the operational semantics of Domain Spe-
cific Visual Languages (DSVLs) [20], taking the advantage
that it is possible to use the concrete syntax of the DSVL in
the rules, which then become more intuitive to the designer.
123

336 J. Cabot et al.
Asmodels andmeta-models can be expressed as graphs (with
typed, attributed nodes and edges), graph transformation can
be used for model manipulation in the MDD approach.
Clearly, the important role of (graph) transformations in
MDD needs to be supported by analysis techniques that help
designers in determining the quality of such transformations.
So far, the main formalization of graph transformation is the
so called algebraic approach [23], which uses category the-
ory in order to express the rewriting. Prominent examples of
this approach are the double [23] and the single [24] pushout
(DPO and SPO), which have developed interesting analysis
techniques, e.g. to check independence between pairs of deri-
vations [23,52], or to calculate critical pairs (minimal context
of pairs of conflicting rules) [28]. However, graph gram-
mar analysis techniques work with simplified meta-mod-
els (so called type graphs), which lack OCL-like constraints
for expressing the well-formedness rules of the meta-model.
By not considering the meta-model constraints, one could
design incorrect rules violating such well-formedness rules.
We believe that integrating OCL constraints and graph trans-
formation is crucial for the applicability of the latter in real
software MDD projects.
In this paper, our goal is to integrate OCL and graph trans-
formation, and provide more advanced analysis techniques
for graph transformations by using OCL as an intermediate
representation to express the semantics of graph transforma-
tion rules. Then, this OCL representation is used to automat-
ically verify the analysis properties of interest.
Representing ruleswithOCL, concepts like attribute com-
putation and attribute conditions in rules can be seamlessly
integrated with the meta-model and its OCL constraints dur-
ing the rule analysis. Moreover, it makes available a plethora
of tools able to analyze this kind of specifications. A sec-
ondary benefit of our approach is that graph transformation
is made available to the increasing number of MDA tools
that the community is building and vice-versa. For example,
by using such MDA tools, it could be possible to (partially)
generate code for the transformations [21], or apply metrics
and redesigns to the rules [37]. In addition, the OCL specifi-
cation derived from graph transformation rules could be used
as a way to add behaviour to meta-models, and contracts for
methods. Finally, an intermediate OCL representation serves
as a neutral language for the integration of different transfor-
mation languages, approaches and tools.
More in detail, we use OCL to represent fully expressive
DPO and SPO rules with negative application conditions and
attribute conditions. In addition, we have represented a num-
ber of analysis properties with OCL, taking into account both
the rule structure and the rule and meta-model constraints.
These properties include rule applicability (whether there is
a model satisfying the rule and the meta-model constraints),
weak executability (whether the rule’s post-condition and
the meta-model constraints are satisfiable by some model)
and strong executability (if a rule applied to a legal model—
which conforms to the meta-model and its well-formedness
constraints—always yields a legal model) among others.
In order to improve the usability of our analysis frame-
work, we have hidden the analysis process behind a graphical
front-end tool called AToM3 [18]. This meta-modelling tool
generates customized modelling environments for DSVLs,
and allows defining model manipulations by graph transfor-
mation. In order to analyse the graph transformation rules,
an OCL generator provides the input to the UMLtoCSP tool
[13] in charge of analyzing the rules’ properties. The results
are then shown back in AToM3 using the concrete syntax of
the DSVL. In this way, the analysis mechanism is kept trans-
parent to the rule designer. This approach follows the line
of hidden formal methods [7], which advocate an intuitive
presentation of the verification results, probably in terms of
the input language.
This paper extends our previous work in [15] by refin-
ing the translation patterns and extending them with a set of
optimization and simplification rules, by adding validation
capabilities to our framework, and by providing a complete
tool support as described above. As part of our tool support
we also discuss some heuristics that help to scale the analysis
when dealing with large meta-models and rules.
Paper Organization. Section2 introduces graph trans-
formation using a production system example. Section3 pre-
sents our translation of graph transformation rules into OCL.
Section4 shows the encoding of some analysis properties for
rule verification and Sect. 5 shows how to use our approach
for validation purposes. Section6 presents the tool support
for the framework. Section7 compares with related work and
Sect. 8 ends with the conclusions. An appendix shows the
OCL translation of all the example rules.
2 Introduction to graph transformation
In this section we give an intuition on graph transforma-
tion by presenting some rules that belong to a simulator of
a DSVL for production systems. Figure1 shows the DSVL
meta-model.
Fig. 1 Meta-model of a DSVL for production systems
123