Case Studies

Because verification of model transformations is a challenging topic in terms of application domains and scalability, one of the primary goal of this year's VOLT edition is the quality of the discussion and cross-fertilisation between different VOLT participants.

After three VOLT editions and a significant number of contributions in the domain of model transformation verification, we see that the community has reached the maturity for comparing different approaches based on common transformation verification cases. Consequently, we propose specific transformation verification cases for this VOLT edition. We strongly encourage the authors to apply these cases for presenting their approaches (e.g., as running examples) or for evaluating their approaches (e.g., as case studies). In the vocabulary of Lucio et al. 2014, the first transformation is a translation (i.e., structural bridge between DSMLs); the second is a translational semantics (i.e., translation with execution delegation); and the third is a simulation (i.e., operational semantics of a DSML).

We hope in this way to stimulate the community towards concrete, reproducible results as well as a first-level comparison of tools and techniques for model transformation verification. For the latter, we plan to organize a post-workshop journal article collecting the results from publications of this year's VOLT edition that are taking any of the cases into consideration.

We will make use of the following transformations which are well-documented in literature:

• Translation case: UML class diagrams to RDBMS Transformation
• Translational semantics case: UML Activity Diagrams to Petri nets Transformation
• Simulation case: Pacman Simulation Transformation

UML class diagrams to RDBMS Transformation Case (CD2RDBMS)

Transformation: This case concerns the classical model transformation example dealing with the generation of relational database schemas from UML class diagrams. For VOLT 2015, we will consider the requirements defined by the Model Transformation in Practice Workshop 2005 (cf. Bézivin et al. 2014) of this transformation.

Properties: For this case, we consider as a starting point three properties the transformation should satisfy with respect to the correspondences between the two modeling languages.

Property 1: Non-persistent classes and non-top classes must not be transformed into a corresponding table.

Property 2: All persistent top classes must be transformed into a corresponding table.

Property 3: Column duplicates are forbidden in the output models, i.e., there should not be two columns with the same name in one table.

UML activity diagrams to Petri nets Transformation Case (AD2PN)

Transformation: This case concerns the mapping from UML activity diagrams into Petri nets as the latter define the execution simulation of the former. For VOLT 2015, we will consider the complete transformation presented in Syriani and Ergin 2012.

Properties: For this case, we consider as a starting point three properties the transformation should satisfy with respect to the analysis of the activity diagram.

Property 1: Exactly one transition is fireable from the initial PN model, as it encodes the behavior of the initial node in AD.

Property 2: If an activity node has its current attribute set to true, then there must be a token in the corresponding place.

Property 3: The entry, exit or transient transition corresponding to an activity node must be L1-live: there exists a firing sequence in which each of these transitions can fire at least once. Therefore, the resulting PN model is deadlock-free.

Pacman Simulation Transformation Case (PACSIM)

Transformation: This case concerns the operational semantics of the Pacman DSML. The original rule-based graph transformation description appeared in Heckel 2006. For VOLT 2015, we refer to the slightly more complex implementation presented in Syriani and Vangheluwe 2012.

Properties: For this case, we consider as a starting point four properties the transformation should satisfy with respect to the execution of an initial Pacman game configuration.

Property 1: All grid nodes containing a pellet (food) object must be reachable by the pacman object.

Property 2: There exists a path where a ghost objects never kills pacman object.

Property 3: A pacman movement rule must be able successfully be applied before the K ghost movement rules are applied. ALternatively, A pacman must move with a time interval I.

Property 4: The pacman object must move within a time interval I.