×

zbMATH — the first resource for mathematics

Formal analysis of model transformations based on triple graph grammars. (English) Zbl 1342.68180
Summary: 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.
MSC:
68Q42 Grammars and rewriting systems
68P15 Database theory
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Term Graph Rewriting: Theory and Practice pp 201– (1993)
[2] DOI: 10.1007/11601548_16 · doi:10.1007/11601548_16
[3] DOI: 10.2307/1968867 · Zbl 0060.12501 · doi:10.2307/1968867
[4] DOI: 10.1051/ita:2005028 · Zbl 1078.18010 · doi:10.1051/ita:2005028
[5] DOI: 10.1016/j.entcs.2005.12.015 · doi:10.1016/j.entcs.2005.12.015
[6] Springer-Verlag Lecture Notes in Computer Science 5765 pp 144– (2010)
[7] Electronic Communications of the EASST 39 pp 1– (2011)
[8] DOI: 10.1007/s10270-008-0089-9 · Zbl 05672218 · doi:10.1007/s10270-008-0089-9
[9] DOI: 10.1007/978-3-642-04425-0_18 · Zbl 05617006 · doi:10.1007/978-3-642-04425-0_18
[10] Bidirectional Programming Languages (2009)
[11] DOI: 10.1007/978-3-540-87405-8_13 · Zbl 1175.68222 · doi:10.1007/978-3-540-87405-8_13
[12] Fundamentals of Algebraic Graph Transformation (2006) · Zbl 1095.68047
[13] DOI: 10.1007/978-3-540-71289-3_7 · Zbl 05270464 · doi:10.1007/978-3-540-71289-3_7
[14] Electronic Communications of the EASST 18 (2009)
[15] DOI: 10.1007/978-3-540-87405-8_29 · Zbl 1175.68114 · doi:10.1007/978-3-540-87405-8_29
[16] DOI: 10.1007/978-3-540-88643-3_10 · Zbl 05365628 · doi:10.1007/978-3-540-88643-3_10
[17] Bulletin of the EATCS 102 pp 111– (2010)
[18] Electronic Communications of the EASST 16 (2009)
[19] DOI: 10.1007/978-3-642-16145-2_9 · Zbl 05827691 · doi:10.1007/978-3-642-16145-2_9
[20] Electronic Communications of the EASST 30 pp 1– (2010)
[21] DOI: 10.1007/978-3-642-15928-2_11 · Zbl 1306.68074 · doi:10.1007/978-3-642-15928-2_11
[22] DOI: 10.1007/978-3-642-24485-8_49 · Zbl 05981806 · doi:10.1007/978-3-642-24485-8_49
[23] DOI: 10.1017/S0960129508007202 · Zbl 1168.68022 · doi:10.1017/S0960129508007202
[24] DOI: 10.1007/11841883_25 · Zbl 1156.68346 · doi:10.1007/11841883_25
[25] Springer-Verlag Lecture Notes in Computer Science 903 pp 151– (1994)
[26] Handbook of Graph Grammars and Computing by Graph Transformations, Volume 1: Foundations (1997) · Zbl 0908.68095
[27] DOI: 10.1007/978-3-642-03741-2_26 · Zbl 1239.68026 · doi:10.1007/978-3-642-03741-2_26
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.