scholarly journals Formal analysis of model transformations based on triple graph grammars

2014 ◽  
Vol 24 (4) ◽  
Author(s):  
FRANK HERMANN ◽  
HARTMUT EHRIG ◽  
ULRIKE GOLAS ◽  
FERNANDO OREJAS
Keyword(s):  
Model Transformation ◽  
Graph Transformation ◽  
Model Transformations ◽  
Graph Grammars ◽  
Attributed Graph ◽  
Translation Rule ◽  
Forward Translation ◽  
Triple Graph Grammars ◽  
Transformation Systems ◽  
Graph Transformation Systems

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 aforward 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.

A NOVEL APPROACH TO VERIFY GRAPH SCHEMA-BASED SOFTWARE SYSTEMS

2009 ◽  
Vol 19 (06) ◽  
pp. 857-870 ◽  
Author(s):  
VAHID RAFE ◽  
ADEL T. RAHMANI
Keyword(s):  
Graph Transformation ◽  
Behavioral Modeling ◽  
Model Transformations ◽  
Software Systems ◽  
Hierarchical Systems ◽  
Input Language ◽  
Novel Approach ◽  
Graph Schema ◽  
Transformation Systems ◽  
Graph Transformation Systems

Graph Grammars have recently become more and more popular as a general formal modeling language. Behavioral modeling of dynamic systems and model to model transformations are a few well-known examples in which graphs have proven their usefulness in software engineering. A special type of graph transformation systems is layered graphs. Layered graphs are a suitable formalism for modeling hierarchical systems. However, most of the research so far concentrated on graph transformation systems as a modeling means, without considering the need for suitable analysis tools. In this paper we concentrate on how to analyze these models. We will describe our approach to show how one can verify the designed graph transformation systems. To verify graph transformation systems we use a novel approach: using Bogor model checker to verify graph transformation systems. The AGG-like graph transformation systems are translated to BIR — the input language of Bogor — and Bogor verifies that model against some properties defined by combining LTL and special purpose graph rules. Supporting schema-based and layered graphs characterize our approach among existing solutions for verification of graph transformation systems.

Combining termination proofs in model transformation systems

2014 ◽  
Vol 24 (4) ◽  
Author(s):  
DÉNES BISZTRAY ◽  
REIKO HECKEL
Keyword(s):  
Model Transformation ◽  
Graph Transformation ◽  
Model Transformations ◽  
Termination Criteria ◽  
Attributed Graphs ◽  
Source Models ◽  
Transformation Systems ◽  
Suitable Technique ◽  
Termination Proofs

In model transformations, where source models are automatically translated into target models or code, termination is necessary for the transformation to be well defined. There are a number of specific termination criteria that can be used when specifying model transformations by graph transformation, though termination is undecidable in general. Unfortunately, and particularly for large and heterogeneous specifications, it is often not possible to use a single termination criterion. In this paper, we propose an approach that applies different criteria to suitable subsets of rules so that termination can be shown locally using the most suitable technique for each subset. Global termination then follows if certain causal dependencies between rules in different subsets are acyclic. The theory is developed at the level of typed attributed graphs, and is motivated and illustrated by a case study translating UML activity diagrams to CSP.

scholarly journals An OCL-Based Framework for Model Transformations

2016 ◽  
Vol 32 (1) ◽  
Author(s):  
Duc-Hanh Dang ◽  
Martin Gogolla
Keyword(s):  
Quality Assurance ◽  
Building Block ◽  
Model Transformation ◽  
Model Transformations ◽  
Graph Grammars ◽  
Object Constraint Language ◽  
Model Driven ◽  
Constraint Language ◽  
Triple Graph Grammars ◽  
Important Building Block

Model transformation is an important building block for model-driven approaches. It puts forward a necessity and a challenge to specify and realize model transformation as well as to ensure the correctness of transformations. This paper proposes an OCL-based framework for model transformations. The formal foundation of the framework is the integration of Triple Graph Grammars and the Object Constraint Language (OCL). The OCL-based transformation framework offers an on-the-fly verification of model transformations and means for transformation quality assurance.

Sign in / Sign up

Export Citation Format

Share Document