Hostname: page-component-76fb5796d-skm99 Total loading time: 0 Render date: 2024-04-26T12:16:32.305Z Has data issue: false hasContentIssue false

Formal analysis of model transformations based on triple graph grammars

Published online by Cambridge University Press:  26 June 2014

FRANK HERMANN
Affiliation:
Institut für Softwaretechnik und Theoretische Informatik, Technische Universität Berlin, Berlin, Germany and Interdisciplinary Centre for Security, Reliability and Trust, University of Luxembourg, Luxembourg Email: frank.hermann@uni.lu
HARTMUT EHRIG
Affiliation:
Institut für Softwaretechnik und Theoretische Informatik, Technische Universität Berlin, Berlin, Germany Email: ehrig@cs.tu-berlin.de
ULRIKE GOLAS
Affiliation:
Konrad-Zuse-Zentrum für Informationstechnik Berlin, Berlin, Germany Email: golas@zib.de
FERNANDO OREJAS
Affiliation:
Departament de Llenguatges i Sistemes Informàtics, Universitat Politècnica de Catalunya, Barcelona, Spain Email: orejas@lsi.upc.edu

Abstract

Triple graph grammars (TGGs) are a well-established concept for the specification and execution of bidirectional model transformations within model driven software engineering. Their main advantage is an automatic generation of operational rules for forward and backward model transformations, which simplifies specification and enhances usability as well as consistency. In this paper we present several important results for analysing model transformations based on the formal categorical foundation of TGGs within the framework of attributed graph transformation systems.

Our first main result shows that the crucial properties of correctness and completeness are ensured for model transformations. In order to analyse functional behaviour, we generate a new kind of operational rule, called a forward translation rule. We apply existing results for the analysis of local confluence for attributed graph transformation systems. As additional main results, we provide sufficient criteria for the verification of functional behaviour as well as a necessary and sufficient condition for strong functional behaviour. In fact, these conditions imply polynomial complexity for the execution of the model transformation. We also analyse information and complete information preservation of model transformations, that is, whether a source model can be reconstructed (uniquely) from the target model computed by the model transformation. We illustrate the results for the well-known model transformation example from class diagrams to relational database models.

Type
Paper
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

AGG (2011) AGG. TFS-Group, TU Berlin. Homepage: www.tfs.tu-berlin.de/agg.Google Scholar
Arendt, T., Biermann, E., Jurack, S., Krause, C. and Taentzer, G. (2010) Henshin: Advanced concepts and tools for in-place EMF model transformations. In: Proceedings of the ACM/IEEE 13th International Conference on Model Driven Engineering Languages and Systems (MoDELS'10). Springer-Verlag Lecture Notes in Computer Science 6394 121135.Google Scholar
Bisztray, D., Heckel, R. and Ehrig, H. (2009) Verification of architectural refactorings: Rule extraction and tool support. Electronic Communications of the EASST 16.Google Scholar
Bohannon, A., Vaughan, J. A. and Pierce, B. C. (2006) Relational Lenses: A Language for Updateable Views. In: Proceedings of the twenty-fifth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems – PODS '06 338–347.CrossRefGoogle Scholar
de Lara, J. and Guerra, E. (2008) Pattern-Based Model-to-Model Transformation. In: Ehrig, H., Heckel, R., Rozenberg, G. and Taentzer, G. (eds.) Proceedings of the 4th International Conference on Graph Transformations (ICGT 2008). Springer-Verlag Lecture Notes in Computer Science 5214 426441.Google Scholar
Ehrig, H., Ehrig, K., Ermel, C., Hermann, F. and Taentzer, G. (2007) Information Preserving Bidirectional Model Transformations. In: Proceedings FASE'07 – Fundamental Approaches to Software Engineering. Springer-Verlag Lecture Notes in Computer Science 4422 7286.Google Scholar
Ehrig, H., Ehrig, K., Prange, U. and Taentzer, G. (2006) Fundamentals of Algebraic Graph Transformation. EATCS Monographs in Theoretical Computer Science, Springer-Verlag.Google Scholar
Ehrig, H., Ermel, C. and Hermann, F. (2008) On the Relationship of Model Transformations Based on Triple and Plain Graph Grammars. In: Proceedings GraMoT'08 – Graph and Model Transformation, ACM 9–16.Google Scholar
Ehrig, H., Ermel, C., Hermann, F. and Prange, U. (2009a) On-the-Fly Construction, Correctness and Completeness of Model Transformations based on Triple Graph Grammars. In: Proceedings MODELS'09 – Model Driven Engineering Languages and Systems. Springer-Verlag Lecture Notes in Computer Science 5795 241255.CrossRefGoogle Scholar
Ehrig, H., Golas, U. and Hermann, F. (2010) Categorical Frameworks for Graph Transformation and HLR Systems based on the DPO Approach. Bulletin of the EATCS 102 111121.Google Scholar
Ehrig, H., Hermann, F. and Sartorius, C. (2009b) Completeness and Correctness of Model Transformations based on Triple Graph Grammars with Negative Application Conditions. Electronic Communications of the EASST 18.Google Scholar
Ehrig, H., Pfender, M. and Schneider, H. (1973) Graph grammars: an algebraic approach. In: 14th Annual IEEE Symposium on Switching and Automata Theory 167–180.Google Scholar
Ehrig, H. and Prange, U. (2008) Formal Analysis of Model Transformations Based on Triple Graph Rules with Kernels. In: Proceedings of the International Conference on Graph Transformation (ICGT'08). Springer-Verlag Lecture Notes in Computer Science 5214 178193.Google Scholar
Foster, J. (2009) Bidirectional Programming Languages, Dissertation, University of Pennsylvania.Google Scholar
Giese, H. and Hildebrandt, S. (2009) Efficient Model Synchronization of Large-Scale Models. Technical Report 28, Hasso Plattner Institute at the University of Potsdam.Google Scholar
Giese, H., Hildebrandt, S. and Lambers, L. (2010) Toward bridging the gap between formal semantics and implementation of triple graph grammars. Technical Report 37, Hasso Plattner Institute at the University of Potsdam.CrossRefGoogle Scholar
Giese, H. and Wagner, R. (2009) From model transformation to incremental bidirectional model synchronization. Software and Systems Modeling 8 (1)2143.Google Scholar
Golas, U., Ehrig, H. and Hermann, F. (2011) Formal Specification of Model Transformations by Triple Graph Grammars with Application Conditions. In: Proceedings of GCM 2010. Electronic Communications of the EASST 39 126.Google Scholar
Guerra, E. and de Lara, J. (2006a) Attributed typed triple graph transformation with inheritance in the double pushout approach. Technical Report UC3M-TR-CS-2006-00, Universidad Carlos III, Madrid, Spain.Google Scholar
Guerra, E. and de Lara, J. (2006b) Model View Management with Triple Graph Grammars. In: Proceedings of the International Conference on Graph Transformation (ICGT'06). Springer-Verlag Lecture Notes in Computer Science 4178 351366.CrossRefGoogle Scholar
Habel, A. and Pennemann, K.-H. (2009) Correctness of high-level transformation systems relative to nested conditions. Mathematical Structures in Computer Science 19 (2)245296.Google Scholar
Hermann, F., Corradini, A. and Ehrig, H. (2014) Analysis of permutation equivalence in $\mathcal{M}$-adhesive transformation systems with negative application conditions. Mathematical Structures in Computer Science (this volume).Google Scholar
Hermann, F., Ehrig, H., Golas, U. and Orejas, F. (2010a) Efficient Analysis and Execution of Correct and Complete Model Transformations Based on Triple Graph Grammars. In: Proceedings MDI'10 – Model Driven Interoperability, ACM 22–31.Google Scholar
Hermann, F., Ehrig, H., Golas, U. and Orejas, F. (2010b) Efficient Analysis and Execution of Correct and Complete Model Transformations Based on Triple Graph Grammars – Extended Version. Technical Report 2010/13, FAk. IV, TU Berlin.Google Scholar
Hermann, F., Ehrig, H., Orejas, F., Czarnecki, K., Diskin, Z. and Xiong, Y. (2011) Correctness of Model Synchronization Based on Triple Graph Grammars. In: Proceedings of the ACM/IEEE 13th International Conference on Model Driven Engineering Languages and Systems (MoDELS'11). Springer-Verlag Lecture Notes in Computer Science 6981 668682.Google Scholar
Hermann, F., Ehrig, H., Orejas, F. and Golas, U. (2010c) Formal Analysis of Functional Behaviour of Model Transformations Based on Triple Graph Grammars. In: Proceedings of the International Conference on Graph Transformation (ICGT' 10). Springer-Verlag Lecture Notes in Computer Science 6372 155170.Google Scholar
Hermann, F., Hülsbusch, M. and König, B. (2010d) Specification and verification of model transformations. Electronic Communications of the EASST 30 121.Google Scholar
Hidaka, S., Hu, Z., Inaba, K., Kato, H., Matsuda, K. and Nakano, K. (2010) Bidirectionalizing graph transformations. In: Proceedings of the 15th ACM SIGPLAN International Conference on Functional programming (ICFP '10) 205–216.Google Scholar
Kindler, E. and Wagner, R. (2007) Triple Graph Grammars: Concepts, Extensions, Implementations, and Application Scenarios. Technical Report tr-ri-07-284, Department of Computer Science, University of Paderborn, Germany.Google Scholar
Klar, F., Lauder, M., Königs, A. and Schürr, A. (2010) Extended Triple Graph Grammars with Efficient and Compatible Graph Translators. In: Graph Transformations and Model Driven Enginering – Essays Dedicated to Manfred Nagl on the Occasion of his 65th Birthday. Springer-Verlag Lecture Notes in Computer Science 5765 144177.Google Scholar
Königs, A. and Schürr, A. (2006) Tool Integration with Triple Graph Grammars – A Survey. In: Proceedings, SegraVis School on Foundations of Visual Modelling Techniques. Electronic Notes in Theoretical Computer Science 148 113150.Google Scholar
Lack, S. and Sobociński, P. (2005) Adhesive and quasiadhesive categories. Theoretical Informatics and Applications 39 (2)511546.Google Scholar
Lambers, L. (2009) Certifying Rule-Based Models using Graph Transformation, Ph.D. thesis, Technische Universität Berlin.Google Scholar
Newman, M. H. A. (1942) On theories with a combinatorial definition of ‘equivalence’. Annals of Mathematics 43 (2)223243.Google Scholar
Orejas, F., Guerra, E., de Lara, J. and Ehrig, H. (2009) Correctness, Completeness and Termination of Pattern-Based Model-to-Model Transformation. In: Kurz, A., Lenisa, M. and Tarlecki, A. (eds.) International Conference on Algebra and Coalgebra in Computer Science (CALCO'09). Springer-Verlag Lecture Notes in Computer Science 5728 383397.Google Scholar
Plump, D. (1993) Hypergraph Rewriting: Critical Pairs and Undecidability of Confluence. In: Term Graph Rewriting: Theory and Practice, John Wiley 201213.Google Scholar
Plump, D. (2005) Confluence of Graph Transformation Revisited. In: Processes, Terms and Cycles: Steps on the Road to Infinity. Springer-Verlag Lecture Notes in Computer Science 3838 280308.Google Scholar
Rozenberg, G. (1997) Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations, World Scientific.Google Scholar
Schürr, A. (1994) Specification of Graph Translators with Triple Graph Grammars. In: Proceedings of the Workshop on Graph-Theoretic Concepts in Computer Science (WG'94). Springer-Verlag Lecture Notes in Computer Science 903 151163.Google Scholar
Schürr, A. and Klar, F. (2008) 15 years of triple graph grammars. In: Proceedings of the International Conference on Graph Transformation (ICGT 2008), 411–425.CrossRefGoogle Scholar
Stevens, P. (2008) A Landscape of Bidirectional Model Transformations. In: Proceedings of GTTSE 2008. Springer-Verlag Lecture Notes in Computer Science 5235 408424.Google Scholar
Taentzer, G.et al. (2005) Model Transformation by Graph Transformation: A Comparative Study. In: Proceedings – Workshop Model Transformation in Practice.Google Scholar