Reusing Model Transformations While Preserving Properties

Abstract. Model transformations are indispensable to model-based development (MBD) where they act as translators between domain-specific languages (DSLs). As a result, transformations must be verified to ensure they behave as desired. Simultaneously, transformations may be reused as requirements evolve. In this paper we present novel algorithms to determine if a reused transformation preserves the same properties as the original, without expensive re-verification. We define a type of behavioral equivalence, called lifting equivalence, relating an original transformation to its reused version. A reused transformation that is equivalent to the original will preserve all compatible universally quantified properties. We describe efficient algorithms for verifying lifting equivalence, which we have implemented in our FORMULA [1, 2] framework.

• Type: Conference
• Year: 2010
• Where: FASE
• Authors: Ethan K. Jackson, Wolfram Schulte, Daniel Balasubramanian, Gabor Karsai
• Keywords: FASE 2010, Model Transformations, Model-based Development, Reused Transformation, Software Engineering