Reusing Model Transformations While Preserving Properties - Jackson, Ethan; Schulte, Wolfram; Balasubramanian, Daniel; Karsai, Gabor (Fundamental Approaches to Software Engineering, 13th International Conference, FASE 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus., 2010)
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 framework.