A Tridimensional Approach for Studying the Formal Verification of Model Transformations

Moussa Amrani (1) , Levi Lucio , Gehan Selim (2) , Benoit Combemale (3) , Jürgen Dingel (2) , Hans Vangheluwe (4) , Yves Le Traon (5) , James R. Cordy (2)

1 LASSY - Laboratory of Advanced Software SYstems [Luxembourg]
2 School of computing [Kingston]
3 TRISKELL - Reliable and efficient component based software engineering
4 PATS - Performance Analysis of Telecommunication Systems Research Group
5 CSC - Computer Science and Communications Research Unit [Luxembourg]

In Model Driven Engineering (MDE), models are first-class citizens, and model transformation is MDE's "heart and soul". Since model transformations are executed for a family of conforming models, their validity becomes a crucial issue. This paper proposes to explore the question of the formal verification of model transformation properties through a tri-dimensional approach: the transformation involved, the properties of interest addressed, and the formal verification techniques used to establish the properties. This work allows a better understanding of the expected properties for a particular transformation, and facilitates the identification of the suitable tools and techniques for enabling their verification.

Domaines: Génie logiciel [cs.SE]

Moussa Amrani, Levi Lucio, Gehan Selim, Benoit Combemale, Jürgen Dingel, et al.. A Tridimensional Approach for Studying the Formal Verification of Model Transformations. Verification and validation Of model Transformations (VOLT), Apr 2012, Montreal, Canada. ⟨hal-00684717⟩