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 |
| Summary: | 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. |
|---|