Formal Analysis of Model Transformations Based on Triple Graph Grammars

in 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 ▲]

Triple Graph Grammars in the Large for Translating Satellite Procedures

in Theory and Practice of Model Transformations (2014, July)

Software translation is a challenging task. Several requirements are important – including automation of the execution, maintainability of the translation patterns, and, most importantly, reliability ... [more ▼]

Software translation is a challenging task. Several requirements are important – including automation of the execution, maintainability of the translation patterns, and, most importantly, reliability concerning the correctness of the translation. Triple graph grammars (TGGs) have shown to be an intuitive, well-defined technique for model translation. In this paper, we leverage TGGs for industry scale software translations. The approach is implemented using the Eclipse-based graph transformation tool Henshin and has been successfully applied in a large industrial project with the satellite operator SES on the translation of satellite control procedures. We evaluate the approach regarding requirements from the project and performance on a complete set of procedures of one satellite. [less ▲]

On Propagation-Based Concurrent Model Synchronization

in Electronic Communications of the EASST (2013), 57

Model transformations based on triple graph grammars (TGGs) have been applied in several practical case studies and they convince by their intuitive and descriptive way of specifying bidirectional model ... [more ▼]

Model transformations based on triple graph grammars (TGGs) have been applied in several practical case studies and they convince by their intuitive and descriptive way of specifying bidirectional model transformations. Moreover, fundamental properties have been extensively studied including syntactical correctness, completeness, termination and functional behaviour. But up to now, it is an open problem how domain specific properties that are valid for a source model can be preserved along model transformations such that the transformed properties are valid for the derived target model. In this paper, we analyse in the framework of TGGs how to propagate constraints from a source model to an integrated and target model such that, whenever the source model satisfies the source constraint also the integrated and target model satisfy the corresponding integrated and target constraint. In our main new results we show under which conditions this is possible. The case study shows how this result is successfully applied for the propagation of security constraints in enterprise modelling between business and IT models. [less ▲]

Satisfaction, Restriction and Amalgamation of Constraints in the Framework of M-Adhesive Categories

in Electronic Proceedings in Theoretical Computer Science (2012), 93

Application conditions for rules and constraints for graphs are well-known in the theory of graph transformation and have been extended already to M-adhesive transformation systems. According to the ... [more ▼]

Application conditions for rules and constraints for graphs are well-known in the theory of graph transformation and have been extended already to M-adhesive transformation systems. According to the literature we distinguish between two kinds of satisfaction for constraints, called general and initial satisfaction of constraints, where initial satisfaction is defined for constraints over an initial object of the base category. Unfortunately, the standard definition of general satisfaction is not compatible with negation in contrast to initial satisfaction. Based on the well-known restriction of objects along type morphisms, we study in this paper restriction and amalgamation of application conditions and constraints together with their solutions. In our main result, we show compatibility of initial satisfaction for positive constraints with restriction and amalgamation, while general satisfaction fails in general. Our main result is based on the compatibility of composition via pushouts with restriction, which is ensured by the horizontal van Kampen property in addition to the vertical one that is generally satisfied in M-adhesive categories [less ▲]

Parallelism and Concurrency of Stochastic Graph Transformations

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 ▲]

Correctness of Model Synchronization Based on Triple Graph Grammars

in Model Driven Engineering Languages and Systems (2011)

Correctness of Model Synchronization Based on Triple Graph Grammars - Extended Version

Report (2011)

Success and efficiency of software and system design fundamentally relies on its models. The more they are based on formal methods the more they can be automatically transformed to execution models and ... [more ▼]

Success and efficiency of software and system design fundamentally relies on its models. The more they are based on formal methods the more they can be automatically transformed to execution models and finally to implementation code. 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. The main purpose of model integration is to establish correspondence between various models, especially between source and target models. From the analysis point of view, model integration supports correctness checks of syntactical dependencies between different views and models. The overall concept is based on the algebraic approach to triple graph grammars, which are widely used for model transformation. The main result shows the close relationship between model transformation and model integration. For each model transformation sequence there is a unique model integration sequence and vice versa. This is demonstrated by a quasi-standard example for model transformation between class models and relational data base models. [less ▲]

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

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 ▲]

Low- and High-Level Petri Nets with Individual Tokens

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 ▲]

Enterprise Modelling using Algebraic Graph Transformation - Extended Version

Report (2010)

An analysis of today's situation at Credit Suisse has shown severe problems, because it is based on current best practices and ad-hoc modelling techniques to handle important aspects of security, risk and ... [more ▼]

An analysis of today's situation at Credit Suisse has shown severe problems, because it is based on current best practices and ad-hoc modelling techniques to handle important aspects of security, risk and compliance. Based on this analysis we propose in this paper a new enterprise model which allows the construction, integration, transformation and evaluation of di erent organizational models in a big decentralized organization like Credit Suisse. The main idea of the new model framework is to provide small decentralized models and intra-model evaluation techniques to handle services, processes and rules separately for the business and IT universe on one hand and for human-centric and machine-centric concepts on the other hand. Furthermore, the new framework provides inter-modelling techniques based on algebraic graph transformation to establish the connection between di erent kinds of models and to allow integration of the decentralized models. In order to check for security, risk and compliance in a suitable way, our models and techniques are based on di erent kinds of formal methods. In this paper, we show that algebraic graph transformation techniques are useful not only for intra-modelling { using graph grammars for visual languages and graph constraints for requirements { but also for inter-modelling { using triple graph grammars for model transformation and integration. Altogether, we present the overall idea of our new model framework and show how to solve speci c problems concerning intra- and inter-modelling as rst steps. This should give evidence that our framework can also ? This work is partially supported by Credit Suisse (Luxembourg) S.A., 56, Grand Rue BP 40, L-1660 Luxembourg, Telephone: +352 46 00 11-1, Fax: +352 46 32 70 handle important other requirements for enterprise modelling in a big decentralized organization like Credit Suisse. [less ▲]