Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Reusing Model Transformations While Preserving Properties

Ethan K. Jackson, Wolfram Schulte, Daniel Balasubramanian, and Gabor Karsai


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.


Publication typeInproceedings
Published inFundamental 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, March 20-28, 2010. Proceedings
SeriesLecture Notes in Computer Science
PublisherSpringer Verlag
> Publications > Reusing Model Transformations While Preserving Properties