Model synchronization based on triple graph grammars: correctness, completeness and invertibility
Triple graph grammars (TGGs) have been used successfully to analyze correctness and completeness of bidirectional model transformations, but a corresponding formal approach to model synchronization has been missing. This paper closes this gap by providing a formal synchronization framework with bidi...
| Authors: | ; ; ; ; ; ; ; |
|---|---|
| Format: | Article |
| Publication date: | 2015 |
| Country: | España |
| Institution: | Universitat Politècnica de Catalunya (UPC) |
| Repository: | UPCommons. Portal del coneixement obert de la UPC |
| Language: | English |
| OAI Identifier: | oai:upcommons.upc.edu:2117/76970 |
| Online Access: | https://hdl.handle.net/2117/76970 https://dx.doi.org/10.1007/s10270-012-0309-1 |
| Access Level: | Open access |
| Keyword: | Formal languages Graph theory Model synchronization Correctness Bidirectional model transformation Triple graph grammars Llenguatges formals Grafs, Teoria de Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica |
| _version_ | 1878740147374129152 |
|---|---|
| author | Hermann, Frank |
| author2 | Ehrig, Hartmut Orejas Valdés, Fernando|||0000-0002-3023-4006 Czarnecki, Krzysztof Diskin, Zinovy Xiong, Yingfei Gottmann, Susann Engel, Thomas |
| author2_role | author author author author author author author |
| author_browse | Czarnecki, Krzysztof Diskin, Zinovy Ehrig, Hartmut Engel, Thomas Gottmann, Susann Hermann, Frank Orejas Valdés, Fernando|||0000-0002-3023-4006 Xiong, Yingfei |
| author_facet | Hermann, Frank Ehrig, Hartmut Orejas Valdés, Fernando|||0000-0002-3023-4006 Czarnecki, Krzysztof Diskin, Zinovy Xiong, Yingfei Gottmann, Susann Engel, Thomas |
| author_role | author |
| collection | UPCommons. Portal del coneixement obert de la UPC |
| description | Triple graph grammars (TGGs) have been used successfully to analyze correctness and completeness of bidirectional model transformations, but a corresponding formal approach to model synchronization has been missing. This paper closes this gap by providing a formal synchronization framework with bidirectional update propagation operations. They are generated from a given TGG, which specifies the language of all consistently integrated source and target models. As our main result, we show that the generated synchronization framework is correct and complete, provided that forward and backward propagation operations are deterministic. Correctness essentially means that the propagation operations preserve and establish consistency while completeness ensures that the operations are defined for all possible inputs. Moreover, we analyze the conditions under which the operations are inverse to each other. All constructions and results are motivated and explained by a running example, which leads to a case study, using concrete visual syntax and abstract syntax notation based on typed attributed graphs. |
| eu_rights_str_mv | openAccess |
| format | article |
| id | ES_ce2581c4e2fe1b3c55e1b06aa2fddd2c |
| institution | Universitat Politècnica de Catalunya (UPC) |
| instname_str | Universitat Politècnica de Catalunya (UPC) |
| language | eng |
| network_acronym_str | ES |
| network_name_str | España |
| oai_identifier_str | oai:upcommons.upc.edu:2117/76970 |
| publishDate | 2015 |
| publishDateSort | 2015 |
| reponame_str | UPCommons. Portal del coneixement obert de la UPC |
| spelling | Model synchronization based on triple graph grammars: correctness, completeness and invertibility Hermann, Frank Ehrig, Hartmut Orejas Valdés, Fernando|||0000-0002-3023-4006 Czarnecki, Krzysztof Diskin, Zinovy Xiong, Yingfei Gottmann, Susann Engel, Thomas Formal languages Graph theory Model synchronization Correctness Bidirectional model transformation Triple graph grammars Llenguatges formals Grafs, Teoria de Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica Triple graph grammars (TGGs) have been used successfully to analyze correctness and completeness of bidirectional model transformations, but a corresponding formal approach to model synchronization has been missing. This paper closes this gap by providing a formal synchronization framework with bidirectional update propagation operations. They are generated from a given TGG, which specifies the language of all consistently integrated source and target models. As our main result, we show that the generated synchronization framework is correct and complete, provided that forward and backward propagation operations are deterministic. Correctness essentially means that the propagation operations preserve and establish consistency while completeness ensures that the operations are defined for all possible inputs. Moreover, we analyze the conditions under which the operations are inverse to each other. All constructions and results are motivated and explained by a running example, which leads to a case study, using concrete visual syntax and abstract syntax notation based on typed attributed graphs. Peer Reviewed https://hdl.handle.net/2117/76970 https://dx.doi.org/10.1007/s10270-012-0309-1 |
| spellingShingle | Model synchronization based on triple graph grammars: correctness, completeness and invertibility Hermann, Frank Formal languages Graph theory Model synchronization Correctness Bidirectional model transformation Triple graph grammars Llenguatges formals Grafs, Teoria de Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica |
| title | Model synchronization based on triple graph grammars: correctness, completeness and invertibility |
| title_full | Model synchronization based on triple graph grammars: correctness, completeness and invertibility |
| title_fullStr | Model synchronization based on triple graph grammars: correctness, completeness and invertibility |
| title_full_unstemmed | Model synchronization based on triple graph grammars: correctness, completeness and invertibility |
| title_short | Model synchronization based on triple graph grammars: correctness, completeness and invertibility |
| title_sort | Model synchronization based on triple graph grammars: correctness, completeness and invertibility |
| topic | Formal languages Graph theory Model synchronization Correctness Bidirectional model transformation Triple graph grammars Llenguatges formals Grafs, Teoria de Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica |
| topic_facet | Formal languages Graph theory Model synchronization Correctness Bidirectional model transformation Triple graph grammars Llenguatges formals Grafs, Teoria de Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica |
| url | https://hdl.handle.net/2117/76970 https://dx.doi.org/10.1007/s10270-012-0309-1 |