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.

PDF file

In  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, March 20-28, 2010. Proceedings

Publisher  Springer Verlag
All copyrights reserved by Springer 2007.

Details