@TechReport{RLK+08-TR,
AUTHOR = {Rangel, Guilherme and Lambers, Leen and König, Barbara and Ehrig, Hartmut and Baldan, Paolo},
TITLE = {{Behavior Preservation in Model Refactoring using DPO Transformations with Borrowed Contexts}},
YEAR = {2008},
NUMBER = {2008-12},
INSTITUTION = {Technische Universitat Berlin},
URL = {http://www.eecs.tu-berlin.de/fileadmin/f4/TechReports/2008/2008-12.pdf},
PDF = {uploads/pdf/RLK+08-TR_2008-12.pdf},
OPTacc_pdf = {},
ABSTRACT = {Behavior preservation, namely the fact that the behavior
of a model is not altered by the transformations, is a crucial property
in refactoring. The most common approaches to behavior preservation
rely basically on checking given models and their refactored versions. In
this paper we introduce a more general technique for checking behavior
preservation of refactorings deØned by graph transformation rules. We
use double pushout (DPO) rewriting with borrowed contexts, and, ex-
ploiting the fact that observational equivalence is a congruence, we show
how to check refactoring rules for behavior preservation. When rules
are behavior-preserving, their application will never change behavior,
i.e., every model and its refactored version will have the same behavior.
However, often there are refactoring rules describing intermediate steps
of the transformation, which are not behavior-preserving, although the
full refactoring does preserve the behavior. For these cases we present
a procedure to combine refactoring rules to behavior-preserving concur-
rent productions in order to ensure behavior preservation. An example
of refactoring for Ønite automata is given to illustrate the theory.}
}