# Formal Analysis of Functional Behaviour for Model Transformations Based on Triple Graph Grammars

@inproceedings{Hermann2010FormalAO, title={Formal Analysis of Functional Behaviour for Model Transformations Based on Triple Graph Grammars}, author={Frank Hermann and Hartmut Ehrig and Fernando Orejas and Ulrike Golas}, booktitle={ICGT}, year={2010} }

Triple Graph Grammars (TGGs) are a well-established concept for the specification of model transformations. In previous work we have formalized and analyzed already crucial properties of model transformations like termination, correctness and completeness, but functional behaviour is missing up to now.
In order to close this gap we generate forward translation rules, which extend standard forward rules by translation attributes keeping track of the elements which have been translated already… Expand

#### 47 Citations

Formal analysis of model transformations based on triple graph grammars

- Mathematics, Computer Science
- Mathematical Structures in Computer Science
- 2014

This paper presents several important results for analysing model transformations based on the formal categorical foundation of TGGs within the framework of attributed graph transformation systems, and generates a new kind of operational rule, called a forward translation rule, for functional behaviour. Expand

Formal Specification of Model Transformations by Triple Graph Grammars with Application Conditions

- Computer Science
- 2011

This paper extends triple rules with a specific form of application conditions, which enhance the expressiveness of formal specifications for model transformations and shows how to extend results concerning information preservation, termi- nation, correctness, and completeness of model transformations to the case with application conditions. Expand

Specification and Verification of Model Transformations

- Computer Science
- Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
- 2010

In order to verify model transformations with respect to behavioural equivalence, well-studied techniques based on the double pushout approach with borrowed context are applied, for which the model transformations specified by triple graph transformation rules are flattened to plain (in-situ)graph transformation rules. Expand

Formal Specification of Model Transformations by Triple Graph Grammars with Application Conditions

- Computer Science
- Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
- 2011

This paper extends triple rules with a specific form of application conditions, which enhance the expressiveness of formal specifications for model transformations and shows how to extend results concerning information preservation, termination, correctness, and completeness of model transformations to the case with application conditions. Expand

Toward Bridging the Gap between Formal Semantics and Implementation of Triple Graph Grammars

- Computer Science
- 2010

This paper captures how the considered TGG implementation realizes the transformation by means of operational rules, define required criteria, and show conformance to the formal semantics if these criteria are fulfilled. Expand

Bridging the gap between formal semantics and implementation of triple graph grammars

- Computer Science
- 2010 Workshop on Model-Driven Engineering, Verification, and Validation
- 2010

This paper captures how the considered TGG implementation realizes the transformation by means of operational rules, define required criteria, and show conformance to the formal semantics if these criteria are fulfilled. Expand

Efficient analysis and execution of correct and complete model transformations based on triple graph grammars

- Computer Science
- MDI '10
- 2010

This paper shows how to improve the efficiency of the execution and analysis of model transformations in practical applications by using triple rules with negative application conditions (NACs). Expand

Model synchronization based on triple graph grammars: correctness, completeness and invertibility

- Computer Science
- Software & Systems Modeling
- 2012

This paper provides a formal synchronization framework with bidirectional update propagation operations generated from a given TGG, which specifies the language of all consistently integrated source and target models. Expand

Correctness of model synchronization based on triple graph grammars

- Computer Science
- MODELS'11
- 2011

This paper provides a formal synchronization framework with bidirectional update propagation operations generated from a TGG, which specifies the language of all consistently integrated source and target models and shows that the generated synchronization framework is correct and complete. Expand

Grammar-based model transformations: Definition, execution, and quality properties

- Computer Science
- Comput. Lang. Syst. Struct.
- 2015

A new approach to model transformation development is proposed which allows to simplify the developed transformations and improve their quality via the exploitation of the languages' structures and it is shown that such transformations have important properties: they terminate and are sound, complete, and deterministic. Expand

#### References

SHOWING 1-10 OF 40 REFERENCES

Formal Analysis of Functional Behaviour for Model Transformations Based on Triple Graph Grammars - Extended Version

- Mathematics
- 2010

Triple Graph Grammars (TGGs) are a well-established concept for the speci cation of model transformations. In previous work we have formalized and analyzed already crucial properties of model… Expand

Completeness and Correctness of Model Transformations based on Triple Graph Grammars with Negative Application Conditions

- Computer Science
- Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
- 2009

This work embeds negative application conditions (NACs) in the concept of triple graph grammars to show completeness and correctness of model transformations based on rules with NACs and furthermore, it can extend the characterization of information preserving model transformations to the case with Nacs. Expand

On-the-Fly Construction, Correctness and Completeness of Model Transformations Based on Triple Graph Grammars

- Computer Science
- MoDELS
- 2009

The new notion of partial source consistency enables us to construct consistent model transformations on-the-fly instead of analyzing consistency of completed model transformations. Expand

On the relationship of model transformations based on triple and plain graph grammars

- Mathematics
- GRaMoT '08
- 2008

Triple graph grammars have been applied and implemented as a formal basis for model transformations in a variety of application areas. They convince by special abilities in automatic derivation of… Expand

Formal Analysis of Model Transformations Based on Triple Graph Rules with Kernels

- Mathematics, Computer Science
- ICGT
- 2008

The relationship between the source consistency of forward transformations, and NAC consistency and termination used in other model transformation approaches is analysed from a formal point of view. Expand

15 Years of Triple Graph Grammars

- Computer Science
- ICGT
- 2008

A more precise formalization of compulsory properties of the translation of triple graph grammars into forward and backward graph translation functions is given and an interpretation and implementation of negative application conditions is derived that does not destroy the benefits of the original approach. Expand

From Model Transformation to Model Integration based on the Algebraic Approach to Triple Graph Grammars

- Computer Science
- Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
- 2008

This paper presents model transformation and model integration as specific problem within bidirectional model transformation, which has shown to support various purposes, such as analysis, optimization, and code generation. Expand

Information Preserving Bidirectional Model Transformations

- Computer Science
- FASE
- 2007

The problem of showing under which condition corresponding forward and backward transformations are inverse to each other in the sense of information preservation is solved in this paper based on general results for the theory of algebraic graph transformations. Expand

Correctness, Completeness and Termination of Pattern-Based Model-to-Model Transformation

- Mathematics, Computer Science
- CALCO
- 2009

This paper studies the compilation into operational triple graph grammar rules and shows correctness of the compilation of a specification without negative patterns, termination of the rules, and completeness, in the sense that every model considered relevant can be built by the rules. Expand

Tool Integration with Triple Graph Grammars - A Survey

- Computer Science
- Electron. Notes Theor. Comput. Sci.
- 2006

This article presents a rule-based approach that allows for the declarative specification of data integration rules and is based on the formalism of triple graph grammars and uses directed graphs to represent MOF-compliant (meta) models. Expand