Specifying and Verifying Semantics-Preserving Model Transformations
-----------------------------------
          
ABSTRACT
-----------------------------------
Model transformations are typically used for defining translations
between modelling languages whose abstract syntaxes are defined by
meta-models. However, model transformations can also be used to give
operational semantics to modelling languages, by acting on their
abstract syntax - just like Structural Operational Semantics rules are
commonly used for defining the operational semantics of programming
languages by acting on their concrete syntax. In this talk we suggest
the definition of mixed graphical-textual language for specifying
model transformations, and give it a formal semantics by mapping it to
the Maude executable specification language. Our intention is that our
language should be intuitive and appear familiar enough to engineers
who know the UML and OCL standards. Using this language, engineers
should be able to write model transformations, which can serve both as
translations between modelling languages and as a means to giving a
formal operational semantics to modelling languages. Then, the natural
question that arises is whether such-defined translations preserve
such-defined operational semantics. We here propose a definition of the
semantics-preservation property based on so-called algebraic stuttering
simulations. Since our property of interest amounts to checking certain
invariance properties of Maude specifications, all techniques available
for proving invariants - state-space exploration, either enumerative or
symbolic, inductive theorem proving, and combinations thereof - can be
used to verify it. An interesting future work direction is to directly
and automatically verify the semantics-preservation property (without
encoding it as an invariance property) using circular coinduction.
          
SPEAKER(S)
-----------------------------------
dr. Vlad RUSU
INRIA (Institut National de Recherche en Informatique et en Automatique)
Rennes
Franta
-----------------------------------
Dr. Vlad Rusu is holding a research position at Irisa/Inria in the Vertecs group.
For more information please visit 
http://www.irisa.fr/vertecs/Equipe/Rusu/
-----------------------------------