Browse ORBi

- 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?

ORBi

Formal Analysis of Model Transformations Based on Triple Graph Grammars Hermann, Frank ; ; et al 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 ▲] Detailed reference viewed: 149 (5 UL)Analysis of Permutation Equivalence in M-adhesive Transformation Systems with Negative Application Conditions Hermann, Frank ; ; in Mathematical Structures in Computer Science (2014), 24(4-09), 1-47 M-adhesive categories provide an abstract framework for a large variety of specification frameworks for modelling distributed and concurrent systems. They extend the well-known frameworks of adhesive and ... [more ▼] M-adhesive categories provide an abstract framework for a large variety of specification frameworks for modelling distributed and concurrent systems. They extend the well-known frameworks of adhesive and weak adhesive HLR categories and integrate high-level constructs such as attribution as in the case of typed attributed graphs. In the current paper, we investigate -adhesive transformation systems including negative application conditions (NACs) for transformation rules, which are often used in applications. For such systems, we propose an original equivalence on transformation sequences, called permutation equivalence, that is coarser than the classical switch equivalence. We also present a general construction of deterministic processes for -adhesive transformation systems based on subobject transformation systems. As a main result, we show that the process obtained from a transformation sequence identifies its equivalence class of permutation-equivalent transformation sequences. Moreover, we show how the analysis of this process can be reduced to the analysis of the reachability graph of a generated Place/Transition Petri net. This net encodes the dependencies between rule applications of the transformation sequence, including the inhibiting effects of the NACs. [less ▲] Detailed reference viewed: 119 (10 UL)Triple Graph Grammars in the Large for Translating Satellite Procedures - Extended Version Hermann, Frank ; Gottmann, Susann ; Nachtigall, Nico et al Report (2014) 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, wellde ned 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 ▲] Detailed reference viewed: 277 (49 UL)Triple Graph Grammars in the Large for Translating Satellite Procedures Hermann, Frank ; Gottmann, Susann ; Nachtigall, Nico et al 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 ▲] Detailed reference viewed: 339 (39 UL)BenchmarX ; ; et al in CEUR Workshop Proceedings (2014, March 28), 1133 Bidirectional transformation (BX) is a very active area of research interest. There is not only a growing body of theory, but also a rich set of tools supporting BX. The problem now arises that there is ... [more ▼] Bidirectional transformation (BX) is a very active area of research interest. There is not only a growing body of theory, but also a rich set of tools supporting BX. The problem now arises that there is no commonly agreed-upon suite of tests or benchmarks that shows either the conformance of tools to theory, or the performance of tools in particular BX scenarios. This paper sets out to improve the state of affairs in this respect, by proposing a template and a set of required criteria for benchmark descriptions, as well as guide- lines for the artifacts that should be provided for each included test. As a proof of concept, the paper additionally provides a detailed description of one concrete benchmark. [less ▲] Detailed reference viewed: 73 (6 UL)Correctness of source code extension for fault detection in openflow based networks Hermann, Frank ; Hommes, Stefan ; State, Radu et al Report (2014) Software Defined Networks using OpenFlow have to provide a re- liable way to detect network faults and attacks. This technical report shows a formal analysis of correctness for an automated code extension ... [more ▼] Software Defined Networks using OpenFlow have to provide a re- liable way to detect network faults and attacks. This technical report shows a formal analysis of correctness for an automated code extension technique used to extend OpenFlow networks with a logging mecha- nism that is used for the detection of faults and attacks. As presented in a companion paper, we applied the code extension techniques for a framework that can extend controller programs transparently, making possible on-line fault management, debugging as well as off-line and forensic analysis. [less ▲] Detailed reference viewed: 175 (37 UL)Solving the FIXML2Code-case Study with HenshinTGG Hermann, Frank ; Nachtigall, Nico ; Braatz, Benjamin et al in Rose, Louis M.; Krause, Christian; Horn, Tassilo (Eds.) Proceedings of the 7th Transformation Tool Contest - part of the Software Technologies: Applications and Foundations (STAF 2014) federation of conferences (2014) Triple graph grammars (TGGs) provide a formal framework for bidirectional model transformations. As in practice, TGGs are primarily used in pure model-to-model transformation scenarios, tools for text-to ... [more ▼] Triple graph grammars (TGGs) provide a formal framework for bidirectional model transformations. As in practice, TGGs are primarily used in pure model-to-model transformation scenarios, tools for text-to-model and model-to-text transformations make them also applicable in text-to-text transformation contexts. This paper presents a solution for the text-to-text transformation case study of the Transformation Tool Contest 2014 on translating FIXML (an XML notation for financial transactions) to source code written in Java, C# or C++. The solution uses the HenshinTGG tool for specifying and executing model-to-model transformations based on the formal concept of TGGs as well as the Xtext tool for parsing XML content to yield its abstract syntax tree (text-to-model transformation) and serialising abstract syntax trees to source code (model-to-text transformation). The approach is evaluated concerning a given set of criteria. [less ▲] Detailed reference viewed: 152 (16 UL)Towards Domain Completeness for Model Transformations Based on Triple Graph Grammars Nachtigall, Nico ; Hermann, Frank ; Braatz, Benjamin et al in Amrani, Moussa; Syriani, Eugene; Wimmer, Manuel (Eds.) Proceedings of the Third International Workshop on Verification of Model Transformations - co-located with Software Technologies: Applications and Foundations (STAF 2014) (2014) The analysis of model transformations is a challenging research area within model driven engineering. Triple graph grammars (TGGs) have been applied in various transformation scenarios and their formal ... [more ▼] The analysis of model transformations is a challenging research area within model driven engineering. Triple graph grammars (TGGs) have been applied in various transformation scenarios and their formal foundation has been a vital ground for general results concerning notions of correctness and completeness. This paper addresses existing gaps between practical scenarios and the formal results of TGGs concerning the notion of completeness. Since the source domain language of a model transformation is usually specified independently from the TGG, we use the notion of domain completeness, which requires that the model transformation has to provide a corresponding target model for each model of the source domain language. As main result, we provide a general method for showing that the source domain language is included in the language that is generated by the source rules of the TGG. This provides the first of two components for verifying domain completeness. The running example is the well studied object-relational mapping. [less ▲] Detailed reference viewed: 92 (12 UL)Automated Source Code Extension for Debugging of OpenFlow based Networks Hommes, Stefan ; Hermann, Frank ; State, Radu et al in Proc. 9th International Conference on Network and Service Management (CNSM) (2013, October) Software-Defined Networks using OpenFlow have to provide a reliable way to to detect network faults in operational environments. Since the functionality of such networks is mainly based on the installed ... [more ▼] Software-Defined Networks using OpenFlow have to provide a reliable way to to detect network faults in operational environments. Since the functionality of such networks is mainly based on the installed software, tools are required in order to determine software bugs. Moreover, network debugging might be necessary in order to detect faults that occurred on the network devices. To determine such activities, existing controller programs must be extended with the relevant functionality. In this paper we propose a framework that can modify controller programs transparently by using graph transformation, making possible online fault management through logging of network parameters in a NoSQL database. Latter acts as a storage system for flow entries and respective parameters, that can be leveraged to detect network anomalies or to perform forensic analysis. [less ▲] Detailed reference viewed: 176 (15 UL)Model synchronization based on triple graph grammars: correctness, completeness and invertibility Hermann, Frank ; ; et al in Software & Systems Modeling (2013) 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 ... [more ▼] 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. [less ▲] Detailed reference viewed: 160 (23 UL)Conformance Analysis of Organizational Models: A New Enterprise Modeling Framework using Algebraic Graph Transformation ; Hermann, Frank in International Journal of Information System Modeling and Design (2013), 4(1), 42-78 Organizational models play a key role in today’s enterprise modeling. They usually show up as partial models produced in a distributed and non-synchronized fashion by people with different conceptual ... [more ▼] Organizational models play a key role in today’s enterprise modeling. They usually show up as partial models produced in a distributed and non-synchronized fashion by people with different conceptual understandings. For this reason, there is a major need to organize partial organizational models within a suitable modeling framework, and, moreover, to check their mutual conformance. This builds the basis to integrate the partial organizational models later on into one holistic model of the organization and for model checking certain security, risk, and compliance constraints. In order to attain this goal, the authors present two mutually aligned contributions. The first one is a new enterprise modeling framework—the EM-Cube. The second one is a new approach for checking conformance of models based on the suggested formal modeling technique associated with the proposed framework. They evaluate the potential solution against concrete requirements derived from a real-world scenario coming out of the finance industry. [less ▲] Detailed reference viewed: 90 (7 UL)Transformation Systems with Incremental Negative Application Conditions ; ; Hermann, Frank et al in Recent Trends in Algebraic Development Techniques (2013) In several application areas, Graph Transformation Systems (GTSs) are equipped with Negative Application Conditions (NACs) that specify “forbidden contexts”, in which the rules shall not be applied. The ... [more ▼] In several application areas, Graph Transformation Systems (GTSs) are equipped with Negative Application Conditions (NACs) that specify “forbidden contexts”, in which the rules shall not be applied. The extension to NACs, however, introduces inhibiting effects among transformation steps that are not local in general, causing a severe problem for a concurrent semantics. In fact, the relation of sequential independence among derivation steps is not invariant under switching, as we illustrate with an example. We first show that this problem disappears if the NACs are restricted to beincremental. Next we present an algorithm that transforms a GTS with arbitrary NACs into one with incremental NACs only, able to simulate the original GTS. We also show that the two systems are actually equivalent, under certain assumptions on NACs. [less ▲] Detailed reference viewed: 129 (18 UL)Towards Bidirectional Engineering of Satellite Control Procedures Using Triple Graph Grammars Gottmann, Susann ; Hermann, Frank ; et al in Jacquet, Christophe; Balasubramanian, Daniel; Jones, Edward (Eds.) et al Proc. Int. Workshop on Multi-Paradigm Modeling 2013 (MPM'13) (2013) The development and maintenance of satellite control software are very complex, mission-critical and cost-intensive tasks that require expertise from different domains. In order to adequately address ... [more ▼] The development and maintenance of satellite control software are very complex, mission-critical and cost-intensive tasks that require expertise from different domains. In order to adequately address these challenges, we propose to use visual views of the software to provide concise abstractions of the system from different perspectives. This paper introduces a visual language for process flow models of satellite control procedures that we developed in cooperation with the industrial partner SES for the satellite control language SPELL. Furthermore, we present a general and formal bidirectional engineering approach for automatically translating satellite control procedures into corresponding process flow visualisations. The bidirectional engineering framework is supported by a visual editor based on Eclipse GMF, the transformation tool HenshinTGG, and additional extensions to meet requirements set up by the specific application area of satellite control languages. [less ▲] Detailed reference viewed: 102 (21 UL)On Propagation-Based Concurrent Model Synchronization ; ; et al 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 ▲] Detailed reference viewed: 103 (6 UL)On an Automated Translation of Satellite Procedures Using Triple Graph Grammars Hermann, Frank ; Gottmann, Susann ; Nachtigall, Nico et al in Duddy, Keith; Kappel, Gerti (Eds.) Theory and Practice of Model Transformations (2013) Model transformation based on triple graph grammars (TGGs) is a general, intuitive and formally well defined technique for the translation of models [5,6,2]. While previous concepts and case studies were ... [more ▼] Model transformation based on triple graph grammars (TGGs) is a general, intuitive and formally well defined technique for the translation of models [5,6,2]. While previous concepts and case studies were focused mainly on visual models of software and systems, this article describes an industrial application of model transformations based on TGGs as a powerful technique for software translation using the tool Henshin [1]. The general problem in this scenario is to translate source code that is currently in use into corresponding source code that shall run on a new system. Up to now, this problem was addressed based on manually written converters, parser generators, compiler-compilers or meta-programming environments using term rewriting or similar techniques (see e. g. [4]). [less ▲] Detailed reference viewed: 188 (22 UL)Correctness and Completeness of Generalised Concurrent Model Synchronisation Based on Triple Graph Grammars Gottmann, Susann ; Hermann, Frank ; Nachtigall, Nico et al in Baudry, Benoit; Dingel, Juergen; Lucio, Levi (Eds.) et al Proc. Int. Workshop on Analysis of Model Transformations 2013 (AMT'13) (2013) Detailed reference viewed: 122 (19 UL)Concurrent Model Synchronization with Conflict Resolution Based on Triple Graph Grammars Hermann, Frank ; ; in J. de Lara, A. Zisman (Ed.) Fundamental Approaches to Software Engineering (2012) Triple graph grammars (TGGs) have been used successfully to analyse correctness of bidirectional model transformations. Recently, also a corresponding formal approach to model synchronization has been ... [more ▼] Triple graph grammars (TGGs) have been used successfully to analyse correctness of bidirectional model transformations. Recently, also a corresponding formal approach to model synchronization has been presented, where updates on a given domain (either source or target) can be correctly (forward or backward) propagated to the other model. However, a corresponding formal approach ofconcurrentmodel synchronization, where a source and a target modification have to be synchronized simultaneously, has not yet been presented and analysed. This paper closes this gap taking into account that the given and propagated source or target model modifications are in conflict with each other. Our conflict resolution strategy is semi-automatic, where a formal resolution strategy – known from previous work – can be combined with a user-specific strategy. As first result, we showcorrectnessof concurrent model synchronization, that is, each result of our nondeterministic concurrent update leads to a consistent correspondence between source and target models, where consistency is defined by the TGG. As second result, we showcompatibilityof concurrent with basic model synchronization: concurrent model synchronization can realize both forward and backward propagation. The results are illustrated by a running example on updating organizational models. [less ▲] Detailed reference viewed: 123 (7 UL)Satisfaction, Restriction and Amalgamation of Constraints in the Framework of M-Adhesive Categories ; ; et al 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 ▲] Detailed reference viewed: 114 (4 UL)On the Concurrent Semantics of Transformation Systems with Negative Application Conditions ; ; Hermann, Frank et al Report (2012) Graph Transformation Systems (GTSs) are an integrated formal speci cation framework for modelling and analysing structural and behavioural aspects of systems. The evolution of a system is modelled by the ... [more ▼] Graph Transformation Systems (GTSs) are an integrated formal speci cation framework for modelling and analysing structural and behavioural aspects of systems. The evolution of a system is modelled by the application of rules to the graphs representing its states and, since typically such rules have local e ects, GTSs are particularly suitable for modelling concurrent and distributed systems where several rules can be applied in parallel. Thus, it is no surprise that a large body of literature is dedicated to the study of the concurrent semantics of graph transformation systems. [less ▲] Detailed reference viewed: 92 (16 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: 112 (8 UL) |
||