Formal Modeling and Analysis of Object Oriented Systems using Triple Graph Grammars

2015 ◽  
Vol 6 (2) ◽  
pp. 48-64 ◽  
Author(s):  
Wafa Chama ◽  
Allaoua Chaoui ◽  
Seidali Rehab
Keyword(s):  
Graph Transformation ◽  
Formal Semantics ◽  
Graph Grammars ◽  
Rewriting Logic ◽  
Modeling Framework ◽  
Modeling Tools ◽  
Modeling And Analysis ◽  
Automatic Translation ◽  
Meta Modeling ◽  
Triple Graph Grammars

This paper proposes a Model Driven Engineering automatic translation approach based on the integration of rewriting logic formal specification and UML semi-formal models. This integration is a contribution in formalizing UML models since it lacks for formal semantics. It aims at providing UML with the capabilities of rewriting logic and its Maude language to control and detect incoherencies in their diagrams. Rewriting logic Maude language allows simulation and verification of system's properties using its LTL model-checker. This automatic translation approach is based on meta-modeling and graph transformation since UML diagrams are graphs. More precisely, the authors have proposed five meta-models and three triple graph grammars to perform the translation process. The authors have used Eclipse Generative Modeling tools: Eclipse Modeling Framework (EMF) for meta-modeling, Graphical Modeling Framework (GMF) for generating visual modeling tools and TGG Interpreter for proposing triple graph grammars. The approach is illustrated through an example.

Unified meta-modeling framework using bond graph grammars for conceptual modeling

2015 ◽  
Vol 72 ◽  
pp. 114-130 ◽  
Author(s):  
Veera Ragavan Sampath Kumar ◽  
Madhavan Shanmugavel ◽  
Velappa Ganapathy ◽  
Bijan Shirinzadeh
Keyword(s):  
Conceptual Modeling ◽  
Bond Graph ◽  
Graph Grammars ◽  
Modeling Framework ◽  
Meta Modeling

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

2012 ◽  
Vol 13 (1) ◽  
pp. 273-299 ◽  
Author(s):  
Holger Giese ◽  
Stephan Hildebrandt ◽  
Leen Lambers
Keyword(s):  
Formal Semantics ◽  
Graph Grammars ◽  
Triple Graph Grammars

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.

Schema Compliant Consistency Management via Triple Graph Grammars and Integer Linear Programming

2021 ◽  
Author(s):  
Nils Weidmann ◽  
Anthony Anjorin
Keyword(s):  
Linear Programming ◽  
Integer Linear Programming ◽  
Experimental Evaluation ◽  
Graph Grammars ◽  
Model Driven Engineering ◽  
Rule Based ◽  
Consistency Management ◽  
Model Driven ◽  
Triple Graph Grammars ◽  
Domain Constraints

AbstractIn the field of Model-Driven Engineering, Triple Graph Grammars (TGGs) play an important role as a rule-based means of implementing consistency management. From a declarative specification of a consistency relation, several operations including forward and backward transformations, (concurrent) synchronisation, and consistency checks can be automatically derived. For TGGs to be applicable in realistic application scenarios, expressiveness in terms of supported language features is very important. A TGG tool is schema compliant if it can take domain constraints, such as multiplicity constraints in a meta-model, into account when performing consistency management tasks. To guarantee schema compliance, most TGG tools allow application conditions to be attached as necessary to relevant rules. This strategy is problematic for at least two reasons: First, ensuring compliance to a sufficiently expressive schema for all previously mentioned derived operations is still an open challenge; to the best of our knowledge, all existing TGG tools only support a very restricted subset of application conditions. Second, it is conceptually demanding for the user to indirectly specify domain constraints as application conditions, especially because this has to be completely revisited every time the TGG or domain constraint is changed. While domain constraints can in theory be automatically transformed to obtain the required set of application conditions, this has only been successfully transferred to TGGs for a very limited subset of domain constraints. To address these limitations, this paper proposes a search-based strategy for achieving schema compliance. We show that all correctness and completeness properties, previously proven in a setting without domain constraints, still hold when schema compliance is to be additionally guaranteed. An implementation and experimental evaluation are provided to support our claim of practical applicability.

UML-BASED MODELING AND ANALYSIS OF SECURITY THREATS

2010 ◽  
Vol 20 (06) ◽  
pp. 875-897 ◽  
Author(s):  
JUN KONG ◽  
DIANXIANG XU ◽  
XIAOQIN ZENG
Keyword(s):  
Formal Method ◽  
Graph Transformation ◽  
State Transitions ◽  
Security Threats ◽  
Sequence Diagrams ◽  
Security Threat ◽  
Initial State ◽  
Final State ◽  
Modeling And Analysis ◽  
Software Application

Poor design has been a major source of software security problems. Rigorous and designer-friendly methodologies for modeling and analyzing secure software are highly desirable. A formal method for software development, however, often suffers from a gap between the rigidity of the method and the informal nature of system requirements. To narrow this gap, this paper presents a UML-based framework for modeling and analyzing security threats (i.e. potential security attacks) rigorously and visually. We model the intended functions of a software application with UML statechart diagrams and the security threats with sequence diagrams, respectively. Statechart diagrams are automatically converted into a graph transformation system, which has a well-established theoretical foundation. Method invocations in a sequence diagram of a security threat are interpreted as a sequence of paired graph transformations. Therefore, the analysis of a security threat is conducted through simulating the state transitions from an initial state to a final state triggered by method invocations. In our approach, designers directly work with UML diagrams to visually model system behaviors and security threats while threats can still be rigorously analyzed based on graph transformation.

Sign in / Sign up

Export Citation Format

Share Document