Specifying and Verifying Semantics-Preserving Model Transformations
22.01.2010 12:00
C308
Vlad Rusu
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.
A. I. Cuza University of Iaşi