Browse ORBilu by Open Access
- What it is and what it isn't
- Green Road / Gold Road?
- Ready to Publish. Now What?
- How can I support the OA movement?
- Where can I learn more?
ORBilu is a project developed by
   Formal Analysis of Model Transformations Based on Triple Graph GrammarsHermann, Frank  ; ; et alin Mathematical Structures in Computer Science (2014), 24(4-08), 1-57 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 ... [more ▼] 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. [less ▲] Detailed reference viewed: 163 (5 UL)Parallelism and Concurrency of Stochastic Graph Transformations; ; et al in Graph Transformations (2012), 7562 Graph transformation systems (GTS) have been proposed for high-level stochastic modelling of dynamic systems and networks. The resulting systems can be described as semi-Markov processes with graphs as ... [more ▼] Graph transformation systems (GTS) have been proposed for high-level stochastic modelling of dynamic systems and networks. The resulting systems can be described as semi-Markov processes with graphs as states and transformations as transitions. The operational semantics of such processes can be explored through stochastic simulation. In this paper, we develop the basic theory of stochastic graph transformation, including generalisations of the Parallelism and Concurrency Theorems and their application to computing the completion time of a concurrent process. [less ▲] Detailed reference viewed: 125 (8 UL) Formal Specification of Model Transformations by Triple Graph Grammars with Application Conditions; ; Hermann, Frank in Electronic Communications of the EASST (2011), 39 Triple graph grammars are a successful approach to describe exogenous model transformations, i.e. transformations between models conforming to different meta-models. Source and target models are related ... [more ▼] Triple graph grammars are a successful approach to describe exogenous model transformations, i.e. transformations between models conforming to different meta-models. Source and target models are related by some connection part, triple rules describe the simultaneous construction of these parts, and forward and backward rules can be derived modeling the forward and backward model transformations. As shown already for the specification of visual models by typed attributed graph transformation, the expressiveness of the approach can be enhanced significantly by using application conditions, which are known to be equivalent to first order logic on graphs. In this paper, we extend triple rules with a specific form of application conditions, which enhance the expressiveness of formal specifications for model transformations. We show how to extend results concerning information preservation, termination, correctness, and completeness of model transformations to the case with application conditions. We illustrate our approach and results with a model transformation from statecharts to Petri nets. [less ▲] Detailed reference viewed: 67 (1 UL)Categorical Frameworks for Graph Transformation and HLR Systems based on the DPO Approach; ; Hermann, Frank in Bulletin of the EATCS (2010), 102 Several variants of high-level replacement (HLR) and adhesive categories have been introduced in the literature as categorical frameworks for graph transformation and HLR systems based on the double ... [more ▼] Several variants of high-level replacement (HLR) and adhesive categories have been introduced in the literature as categorical frameworks for graph transformation and HLR systems based on the double pushout (DPO) approach. In addition to HLR, adhesive, and adhesive HLR categories several weak variants, especially weak adhesive HLR with horizontal and vertical variants, as well as partial variants, including partial map adhesive and partial VK square adhesive categories are reviewed and related to each other. We propose as weakest version the class of vertical weak adhesive HLR categories, short $\mathcalM$-adhesive categories, which are still sufficient to obtain most of the main results for graph transformation and HLR systems. The results in this paper are summarized in Fig.~f:hierarchy showing a hierarchy of all these variants of adhesive, adhesive HLR, and $\mathcalM$-adhesive categories, which can be considered as different categorical frameworks for graph transformation and HLR systems. [less ▲] Detailed reference viewed: 86 (3 UL) Efficient Analysis and Execution of Correct and Complete Model Transformations Based on Triple Graph Grammars - Extended VersionHermann, Frank ; ; et alReport (2010) Triple Graph Grammars are a well-established, formal and intuitive concept for the specification and analysis of bidirectional model transformations. In previous work we have formalized and analyzed ... [more ▼] Triple Graph Grammars are a well-established, formal and intuitive concept for the specification and analysis of bidirectional model transformations. In previous work we have formalized and analyzed already termination, correctness, completeness, local confluence and functional behaviour. In this paper, we show 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). In addition to specification NACs, which improve the specification of model transformations, the generation of filter NACs improves the efficiency of the execution and the analysis of functional behaviour supported by critical pair analysis of the tool AGG. We illustrate the results for the well-known model transformation from class diagrams to relation database models. [less ▲] Detailed reference viewed: 72 (2 UL)Efficient Analysis and Execution of Correct and Complete Model Transformations Based on Triple Graph GrammarsHermann, Frank ; ; et alin Bézivin, Jean; Soley, R.M.; Vallecillo, A. (Eds.) Proc. Int. Workshop on Model Driven Interoperability (MDI'10) (2010) Triple Graph Grammars are a well-established, formal and intuitive concept for the specification and analysis of bidirectional model transformations. In previous work we have formalized and analyzed ... [more ▼] Triple Graph Grammars are a well-established, formal and intuitive concept for the specification and analysis of bidirectional model transformations. In previous work we have formalized and analyzed already termination, correctness, completeness, local confluence and functional behaviour. In this paper, we show 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). In addition to specification NACs, which improve the specification of model transformations, the generation of filter NACs improves the efficiency of the execution and the analysis of functional behaviour supported by critical pair analysis of the tool AGG. We illustrate the results for the well-known model transformation from class diagrams to relational database models. [less ▲] Detailed reference viewed: 95 (1 UL)Formal Analysis of Functional Behaviour of Model Transformations Based on Triple Graph GrammarsHermann, Frank ; ; et alin Graph Transformation (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 ... [more ▼] 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. In the first main result we show the equivalence of model transformations based on forward resp. forward translation rules. This way, an additional control structure for the forward transformation is not needed. This allows to apply critical pair analysis and corresponding tool support by the tool AGG. However, we do not need general local confluence, because confluence for source graphs not belonging to the source language is not relevant for the functional behaviour of a model transformation. For this reason we only have to analyze a weaker property, called translation confluence. This leads to our second main result, the functional behaviour of model transformations, which is applied to our running example, the model transformation from class diagrams to database models. [less ▲] Detailed reference viewed: 93 (4 UL)Low- and High-Level Petri Nets with Individual Tokens; ; et al Report (2010) In this article, we present a new variant of Petri nets with markings called Petri nets with individual tokens, together with rule-based transformation following the double pushout approach. The most ... [more ▼] In this article, we present a new variant of Petri nets with markings called Petri nets with individual tokens, together with rule-based transformation following the double pushout approach. The most important change to former Petri net transformation approaches is that the marking of a net is no longer a collective set of tokens, but each each has an own identity leading to the concept of Petri nets with individual tokens. This allows us to formulate rules that can change the marking of a net arbitrarily without necessarily manipulating the structure. As a first main result that depends on nets with individual markings we show the equivalence of transition firing steps and the application of firing-simulating rules. We define categories of low-level and of algebraic high-level nets with individual tokens, called PTI nets and AHLI nets, respectively and relate them with each other and their collective counterparts by functors. To be able to use the properties and analysis results of \MCALM-adhesive HLR systems (formerly know as weak adhesive high-level replacement systems) we show in further main results that both categories of PTI nets and AHLI nets are \MCALM-adhesive categories. By showing how to construct initial pushouts we also give necessary and sufficient conditions for the applicability of transformation rules in these categories, known as gluing condition in the literature. [less ▲] Detailed reference viewed: 134 (5 UL) |
||
