Levi L�cio

DSLTrans

DSLTrans is model transformation language aimed at performing translations. A transformation with the translation intent is a transformation that translates the meaning of models conforming to a source metamodel into models conforming to a target metamodel. The target can then be used to achieve several tasks that are difficult, or sometimes impossible, to perform on the original input. The cornerstone of DSLTrans is that it is Turing Incomplete. In other words, DSLTrans avoids constructs which imply unbounded recursion or non-determinism, thus making DSLTrans transformations easy to write in a clean fashion, but more importantly, possible to verify formally. This expressiveness reduction does not affect the implementability of transformations with the translation intent. As a proof of concept, you can take a look at transformation examples of UML to Java and Statecharts to APN.

I have developed the formal semantics of DSLTrans based on structural operational semantics and mathematically proved using those same semantics that every DSLTrans transformation terminates and is confluent. You can find the paper describing the theory here.

Bruno Barroca and Cl�udio Gomes from the University Nova de Lisboa have implemented the DSLTrans model transformation language as an Eclipse Plugin.

Download DSLTrans here.

SyVOLT

SyVOLT (SYmbolic Verification Of modeL Transformations) is symbolic execution based technique I have developed for proving syntax model relation properties of model transformations. Such properties are expressed as in the literature as precondition-postcondition axioms involving statements about the syntactic structure of the input and output models of a transformation. The theory behind the approach is described here. We have proved that the symbolic execution of any DSLTrans model transformation is a finite object. The theory capitalises on the fact that transformations written in DSLTrans terminate and are confluent by construction.

Based on the theory mentioned above I have built a Python based prototype of the approach based on the T-Core model transformation framework. The prototype has been developed according to Model Driven Development (MDD) principles and uses AToM³ for metamodelling and modelling the necessary artifacts. The symbolic execution construction, property proof algorithms and experiment results are described in detail here .

Download SyVOLT here.

Check out this video for an overall description of SyVOLT.