×

Behavior preservation in model refactoring using DPO transformations with borrowed contexts. (English) Zbl 1175.68231

Ehrig, Hartmut (ed.) et al., Graph transformations. 4th international conference, ICGT 2008, Leicester, United Kingdom, September 7–13, 2008. Proceedings. Berlin: Springer (ISBN 978-3-540-87404-1/pbk). Lecture Notes in Computer Science 5214, 242-256 (2008).
Summary: 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 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. 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 concurrent productions in order to ensure behavior preservation. An example of refactoring for finite automata is given to illustrate the theory.
For the entire collection see [Zbl 1148.68002].

MSC:

68Q42 Grammars and rewriting systems
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Mens, T.; Gorp, P. V., A taxonomy of model transformation, ENTCS, 152, 125-142 (2006)
[2] Mens, T.; Tourwe, T., A survey of software refactoring, IEEE Transactions on Software Engineering, 30, 2, 126-139 (2004) · doi:10.1109/TSE.2004.1265817
[3] Rangel, G., König, B., Ehrig, H.: Bisimulation verification for the DPO approach with borrowed contexts. In: Proc. of GT-VMT 2007. Electronic Communications of the EASST, vol. 6 (2007)
[4] Biermann, E., Ehrig, K., Köhler, C., Kuhns, G., Taentzer, G., Weiss, E.: EMF model refactoring based on graph transformation concepts. In: SeTra 2006. Electronic Communications of EASST, vol. 3 (2006)
[5] Hoffmann, B.; Janssens, D.; Eetvelde, N. V., Cloning and expanding graph transformation rules for refactoring, ENTCS, 152, 53-67 (2006)
[6] Mens, T.; Taentzer, G.; Runge, O., Analysing refactoring dependencies using graph transformation, Software and Systems Modeling, 6, 3, 269-285 (2007) · doi:10.1007/s10270-006-0044-6
[7] van Kempen, M., Chaudron, M., Kourie, D., Boake, A.: Towards proving preservation of behaviour of refactoring of UML models. In: SAICSIT 2005, South African Institute for Computer Scientists and Information Technologists, pp. 252-259 (2005)
[8] Pérez, J., Crespo, Y.: Exploring a method to detect behaviour-preserving evolution using graph transformation. In: Proceedings of the Third International ERCIM Workshop on Software Evolution, pp. 114-122 (2007)
[9] Narayanan, A., Karsai, G.: Towards verifying model transformations. In: Bruni, R., Varró, D. (eds.) Proc. of GT-VMT 2006, Vienna. ENTCS, pp. 185-194 (2006) · Zbl 1283.68210
[10] Van Gorp, P.; Stenten, H.; Mens, T.; Demeyer, S.; Stevens, P.; Whittle, J.; Booch, G., Towards automating source-consistent UML refactorings, «UML» 2003 - The Unified Modeling Language. Modeling Languages and Applications, 144-158 (2003), Heidelberg: Springer, Heidelberg
[11] Bisztray, D.; Heckel, R.; Ehrig, H.; Fiadeiro, J. L.; Inverardi, P., Verification of architectural refactorings by rule extraction, Fundamental Approaches to Software Engineering, 347-361 (2008), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-540-78743-3_26
[12] Ehrig, H.; König, B.; Walukiewicz, I., Deriving bisimulation congruences in the DPO approach to graph rewriting, Foundations of Software Science and Computation Structures, 151-166 (2004), Heidelberg: Springer, Heidelberg · Zbl 1126.68446
[13] Hirschkoff, D., Bisimulation verification using the up-to techniques, International Journal on Software Tools for Technology Transfer, 3, 3, 271-285 (2001) · Zbl 0991.68052
[14] Ehrig, H.; Ehrig, K.; Prange, U.; Taentzer, G., Fundamentals of Algebraic Graph Transformation (2006), New York: Springer, New York · Zbl 1095.68047
[15] Lambers, L.: Adhesive high-level replacement system with negative application conditions. Technical report, TU Berlin (2007)
[16] Rangel, G., Lambers, L., König, B., Ehrig, H., Baldan, P.: Behavior preservation in model refactoring using DPO transformations with borrowed contexts. Technical Report 12/08, TU Berlin (2008) · Zbl 1175.68231
[17] Ehrig, H.; König, B., Deriving bisimulation congruences in the DPO approach to graph rewriting with borrowed contexts, Mathematical Structures in Computer Science, 16, 6, 1133-1163 (2006) · Zbl 1107.68055 · doi:10.1017/S096012950600569X
[18] Corradini, A.; Montanari, U.; Rossi, F.; Ehrig, H.; Heckel, R.; Loewe, M.; Rozenberg, G., Algebraic approaches to graph transformation part I: Basic concepts and double pushout approach, Handbook of Graph Grammars and Computing by Graph transformation, Foundations, 163-246 (1997), Singapore: World Scientific, Singapore · Zbl 0908.68095
[19] Rangel, G.: Bisimulation Verification for Graph Transformation Systems with Borrowed Contexts. PhD thesis, TU Berlin (to appear, 2008)
[20] Rangel, G.; König, B.; Ehrig, H.; Amadio, R., Deriving bisimulation congruences in the presence of negative application conditions, Foundations of Software Science and Computational Structures, 413-427 (2008), Heidelberg: Springer, Heidelberg · Zbl 1139.68043 · doi:10.1007/978-3-540-78499-9_29
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.