Abstract
The correctness of model transformations is a crucial element for model-driven engineering of high quality software. In particular, behavior preservation is the most important correctness property avoiding the introduction of semantic errors during the model-driven engineering process. Behavior preservation verification techniques either show that specific properties are preserved, or more generally and complex, they show some kind of bisimulation between source and target model of the transformation. Both kinds of behavior preservation verification goals have been presented with automatic tool support for the instance level, i.e. for a given source and target model specified by the model transformation. However, up until now there is no automatic verification approach available at the transformation level, i.e. for all source and target models specified by the model transformation. In this paper, we present a first approach towards automatic behavior preservation verification for model transformations specified by triple graph grammars and semantic definitions given by graph transformation rules. In particular, we show that the behavior preservation problem can be reduced to invariant checking for graph transformation. We discuss today’s limitations of invariant checking for graph transformation and motivate further lines of future work in this direction.
This work was funded by the Deutsche Forschungsgemeinschaft in the course of the project - Correct Model Transformations - see http://www.hpi.uni-potsdam.de/giese/ projekte/kormoran.html?L=1 .
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Milner, R.: Communication and Concurrency. Prentice Hall International (UK) Ltd., Hertfordshire (1995)
Varró, D., Pataricza, A.: Automated Formal Verification of Model Transformations. In: Jürjens, J., Rumpe, B., France, R., Fernandez, E.B. (eds.) CSDUML 2003: Critical Systems Development in UML; Proceedings of the UML 2003 Workshop. Number TUM-I0323 in Technical Report, Technische Universitat Munchen, pp. 63–78 (September 2003)
Engels, G., Kleppe, A., Rensink, A., Semenyak, M., Soltenborn, C., Wehrheim, H.: From UML Activities to TAAL - Towards Behaviour-Preserving Model Transformations. In: Schieferdecker, I., Hartman, A. (eds.) ECMDA-FA 2008. LNCS, vol. 5095, pp. 94–109. Springer, Heidelberg (2008)
Narayanan, A., Karsai, G.: Verifying Model Transformations by Structural Correspondence. Electronic Communications of the EASST: Graph Transformation and Visual Modeling Techniques 2008 10 (2008)
Giese, H., Glesner, S., Leitner, J., Schäfer, W., Wagner, R.: Towards Verified Model Transformations. In: Hearnden, D., Süß, J., Baudry, B., Rapin, N. (eds.) Proc. of the 3rd International Workshop on Model Development, Validation and Verification (MoDeV2a). Genova, Italy, Le Commissariat à l’Energie Atomique - CEA, pp. 78–93 (October 2006)
Hülsbusch, M., König, B., Rensink, A., Semenyak, M., Soltenborn, C., Wehrheim, H.: Showing Full Semantics Preservation in Model Transformation - A Comparison of Techniques. In: Méry, D., Merz, S. (eds.) IFM 2010. LNCS, vol. 6396, pp. 183–198. Springer, Heidelberg (2010)
Rangel, G., Lambers, L., König, B., Ehrig, H., Baldan, P.: Behavior Preservation in Model Refactoring using DPO Transformations with Borrowed Contexts. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 242–256. Springer, Heidelberg (2008)
Bisztray, D., Heckel, R., Ehrig, H.: Compositional Verification of Architectural Refactorings. In: de Lemos, R., Fabre, J.-C., Gacek, C., Gadducci, F., ter Beek, M. (eds.) Architecting Dependable Systems VI. LNCS, vol. 5835, pp. 308–333. Springer, Heidelberg (2009)
Schürr, A.: Specification of Graph Translators with Triple Graph Grammars. In: Mayr, E.W., Schmidt, G., Tinhofer, G. (eds.) WG 1994. LNCS, vol. 903, pp. 151–163. Springer, Heidelberg (1995)
Becker, B., Beyer, D., Giese, H., Klein, F., Schilling, D.: Symbolic Invariant Verification for Systems with Dynamic Structural Adaptation. In: Proc. of the 28th International Conference on Software Engineering (ICSE), Shanghai, China. ACM Press (2006)
Becker, B., Lambers, L., Dyck, J., Birth, S., Giese, H.: Iterative Development of Consistency-Preserving Rule-Based Refactorings. In: Cabot, J., Visser, E. (eds.) ICMT 2011. LNCS, vol. 6707, pp. 123–137. Springer, Heidelberg (2011)
Giese, H., Hildebrandt, S., Lambers, L.: Bridging the Gap Between Formal Semantics and Implementation of Triple Graph Grammars - Ensuring Conformance of Relational Model Transformation Specifications and Implementations. Software and Systems Modeling (2012)
Golas, U., Lambers, L., Ehrig, H., Giese, H.: Toward Bridging the Gap between Formal Foundations and Current Practice for Triple Graph Grammars. In: Ehrig, H., Engels, G., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2012. LNCS, vol. 7562, pp. 141–155. Springer, Heidelberg (2012)
Habel, A., Pennemann, K.H.: Correctness of high-level transformation systems relative to nested conditions. Mathematical Structures in Computer Science 19, 1–52 (2009)
Ehrig, H., Golas, U., Habel, A., Lambers, L., Orejas, F.: M-adhesive transformation systems with nested application conditions, part 1: Parallelism, concurrency and amalgamation. Mathematical Structures in Computer Science (to appear, 2012)
Habel, A., Heckel, R., Taentzer, G.: Graph Grammars with Negative Application Conditions. Fundamenta Informaticae 26(3/4), 287–313 (1996)
Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Springer (2006)
Ermel, C., Gall, J., Lambers, L., Taentzer, G.: Modeling with Plausibility Checking: Inspecting Favorable and Critical Signs for Consistency between Control Flow and Functional Behavior. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol. 6603, pp. 156–170. Springer, Heidelberg (2011)
Pennemann, K.H.: Development of Correct Graph Transformation Systems. PhD thesis, Department of Computing Science, University of Oldenburg, Oldenburg (2009)
Charpentier, M.: Composing Invariants. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 401–421. Springer, Heidelberg (2003)
Ehrig, H., Habel, A., Lambers, L.: Parallelism and Concurrency Theorems for Rules with Nested Application Conditions. In: Festschrift dedicated to Hans-Jorg Kreowski at the Occasion of his 60th Birthday. EC-EASST, vol. 26 (2010)
Lambers, L.: Certifying Rule-Based Models using Graph Transformation. PhD thesis, Technische Universität Berlin (2010)
Orejas, F., Ehrig, H., Prange, U.: A Logic of Graph Constraints. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 179–198. Springer, Heidelberg (2008)
Blume, C., Bruggink, H.S., König, B.: Recognizable Graph Languages for Checking Invariants. In: Proc. of GT-VMT 2010 (Workshop on Graph Transformation and Visual Modeling Techniques). Electronic Communications of the EASST, vol. 29 (2010)
Cabot, J., Clarisó, R., Guerra, E., Lara, J.: Verification and validation of declarative model-to-model transformations through invariants. J. Syst. Softw. 83(2), 283–302 (2010)
Frias, M.F., Galeotti, J.P., Pombo, C.L., Aguirre, N.: DynAlloy: Upgrading Alloy with actions. In: Proc. of Int. Conf. of Software Engineering, pp. 442–451. ACM (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Giese, H., Lambers, L. (2012). Towards Automatic Verification of Behavior Preservation for Model Transformation via Invariant Checking. In: Ehrig, H., Engels, G., Kreowski, HJ., Rozenberg, G. (eds) Graph Transformations. ICGT 2012. Lecture Notes in Computer Science, vol 7562. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33654-6_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-33654-6_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33653-9
Online ISBN: 978-3-642-33654-6
eBook Packages: Computer ScienceComputer Science (R0)