@InProceedings{RLK+08,
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},
BOOKTITLE = {Proc. International Conference on Graph Transformation (ICGT'08)},
VOLUME = {5214},
PAGES = {242--256},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Heidelberg},
PUBLISHER = {Springer},
PDF = {uploads/pdf/RLK+08_refact_pc.pdf},
OPTacc_pdf = {},
ABSTRACT = {Behavior preservation, namely the fact that the behavior of a model is not altered along the transformations, is a crucial property in refactoring. The most common approaches to behavior preservation rely basically on checking given instances of a model class and their refactored versions. In this paper we introduce a more general technique for checking behavior preservation of refactorings defined by graph transformation rules. We use double pushout (DPO) rewriting with borrowed contexts, and, exploiting the fact that observational equivalence is a congruence, we show how to check refactoring rules for behavior preservation without the need of considering specific instances of the model. When rules are behavior-preserving, their application will never change behavior, i.e., every instance of the model class 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 concurrent productions in order to ensure behavior preservation. An example of refactoring for finite automata is given to illustrate the theory.}
}