Search

The project Safe Pointers by Graph Transformation at the University of York has developed a method for specifying the shape of pointer-data structures by graph reduction, and a static checking algorithm for proving the shape safety of graph transformation rules modelling operations on pointer structures. In this paper, we outline how to apply this approach to the C programming language. We extend ANSI C with so-called transformers which model graph transformation rules, and with shape specifications for pointer structures. For the resulting language C-GRS, we present both a translation to C and and an abstraction to graph transformation. Our main result is that the abstraction of transformers to graph transformation rules is correct in that the C code implementing transformers is compatible with the semantics of graph transformation.

We describe the design and the present state of the verification tool Augur 2 which is currently being developed. It is based on Augur 1, a tool which can analyze graph transformation systems by approximating them by Petri nets. The main reason for the new development was to create an open, flexible and extensible verification environment. Also, compared to the previous version, Augur 2 will include more functionality and new analysis techniques.

This paper examines left-linear non-orthogonal term graph rewriting systems that allow asymmetric conflicts between redexes. Using a definition of compatibility of sequences based on Boudol's work on the semantics of term rewriting, it shows that two properties associated with functional languages are true of such graph rewriting systems. First, that a notion of standard computation can be defined and that an associated standardisation theorem can be proved. Second, that a set of events can be associated with a reduction sequence and hence event structures modelling all the possible reduction sequences from a given initial graph can be constructed.

Refactoring is a software engineering technique that aims at enhancing the structure of object-oriented software while preserving its behavior. Several authors have studied how graph transformation can be used to specify refactoring, because such specifications are more precise and can thus, in principle, easier be verified to preserve a program's behavior. It has turned out that “standard” ways of graph transformation do not suffice to define refactoring: their expressive power must be increased if they shall be useful in this application area. Two mechanisms have been proposed so far: one for cloning, and one for expanding nodes by graphs. However, the mechanisms and notations needed are rather complex. In this paper we provide, in the context of double pushout graph transformation, a more elegant and intuitive description. It is based on a notion of rule instantiation, where the instantiation transforms rule schemes into rule instances by cloning and expansion. The power of the technique is demonstrated by an application to two well-known refactoring operations.

This work discusses the state-of-the-art of visual editor generation based on graph transformation concepts on one hand, and using the Eclipse technology which includes the Graphical Editor Framework (GEF), on the other hand. Due to existing shortcomings in both approaches, we present a combined approach for a tool environment that allows to generate a GEF-based editor from a formal, graph-transformation based visual language specification.

Process calculi with various signatures and reaction rules may provide a theoretical basis for pervasive computing.

Reasoning about graph and model transformation systems is an important means to underpin model-driven software engineering, such as Model-Driven Architecture (MDA) and Model Integrated Computing (MIC). Termination criteria for graph and model transformation systems have become a focused area recently. This paper provides termination criteria for graph and model transformation systems with injective matches and finite input structure. It proposes a treatment for infinite sequences of rule applications, and takes attribute conditions, negative application conditions, and type constraints into account. The results are illustrated on case studies excerpted from real-world transformations, which show the termination properties of the frequently used "transitive closure" and "leaf collector" transformation idioms. An intuitive comparison with other approaches is also given.

Sharing graphs are a brilliant solution to the implementation of Lévy optimal reductions of λ-calculus. Sharing graphs are interesting on their own and optimal sharing reductions are just a particular reduction strategy of a more general sharing reduction system.The paper is a gentle introduction to sharing graphs and tries to confute some of the common myths on the difficulty of sharing implementations.

Model transformation means converting an input model available at the beginning of the transformation process to an output model. A widely used approach to model transformation uses graph rewriting as the underlying transformation technique. In case of diagrammatic languages, such as the Unified Modeling Language (UML), the exclusive topological matching is found to be not enough. To define precisely the transformation steps beyond the topology of the visual models, additional constraints must be specified which ensures the correctness of the attributes, or other properties to be enforced. Dealing with OCL constraints provides a solution for these unsolved issues, because topological and attribute transformation methods cannot perform and express the problems which can be addressed by constraint validation. The use of OCL as a constraint and query language in modeling is essential. We have shown that it can be applied to model transformations as well. Often, the same constraint is repetitiously applied in many different places in a transformation. It would be beneficial to describe a common constraint in a modular manner, and to designate the places where it is to be applied. This paper presents the problem of crosscutting constraints in transformation rules, and provides an aspect-oriented solution for it. Our approach makes it possible to define constraints separately from the transformation steps, and facilitates specifying their propagation assignment to graph transformation rules. To illustrate the conceptual results, a case study is also provided, which introduces (i) how our approach generates user interface handler source code for mobile platform from a resource model and a statechart diagram, and (ii) how it validates specific properties during the transformation steps using aspect-oriented constraints.

The tracer Hat records in a detailed trace the computation of a program written in the lazy functional language Haskell. The trace can then be viewed in various ways to support program comprehension and debugging. The trace was named the augmented redex trail. Its structure was inspired by standard graph rewriting implementations of functional languages. Here we describe a model of the trace that captures its essential properties and allows formal reasoning. The trace is a graph constructed by graph rewriting but goes beyond simple term graphs. Although the trace is a graph whose structure is independent of any rewriting strategy, we define the trace inductively, thus giving us a powerful method for proving its properties.

With the growing importance of model-driven development, the ability of transforming models into well-defined semantic domains becomes a key to automated code generation or verification in the software development process. In this paper, we describe a high-level concept for specifying model transformations by means of typed, attributed graph transformation at the level of formal visual language specifications for the source and the target language. At the implementation level, a graph-transformation based generator of visual editor Eclipse plug-ins from formal visual language specifications has been developed. On the basis of this generator we discuss concepts for an implementation of the presented model transformation concepts and for an integration with the generated Eclipse plug-ins. We explain the concepts for model transformation and their implementation along a concrete model transformation from activity diagrams to Petri nets.

Visual rewriting techniques, in particular graph transformations, are increasingly used to model transformations of systems specified through diagrammatic sentences. Several rewriting models have been proposed, differing in the expressivity of the types of rules and in the complexity of the rewriting mechanism; yet basic results concerning the formal properties of these models are still missing for many of them. In this paper, we propose a contribution towards solving the termination problem for rewriting systems with external control mechanisms. In particular, we obtain results of more general validity by extending the concept of transformation unit to high-level replacement systems, a generalization of graph transformation systems. For high-level replacement units, we state and prove several abstract properties based on termination criteria. Then, we instantiate the high-level replacement systems by attributed graph transformation systems and present concrete termination criteria. These are used to show the termination of some replacement units needed to express model transformations as a consequence of software refactoring.

International audience; We tackle the problem of data-structure rewriting including global and local pointerredirections. Each basic rewrite step may perform three kinds of actions: (i) Local redirection, the aim of which is to redirect specific pointers determined by means of a pattern; (ii) Replacement, that may add new information to data-structures; (iii) Global redirection, which is aimed at redirecting all pointers targeting a node towards another one. We define a new framework, following the double-pushout approach, where graph rewrite rules may mix these three kinds of actions in a row. We define first the category of graphs we consider and then we define rewrite rules as pairs of graph homomorphisms of the form L←K→R. In our setting, graphK is not arbitrary, it is used to encode pointerredirection. Furthermore, pushouts do not always exist and complement pushouts, when they exist, are not unique. Despite these concerns, our definition of rewriting steps is such that a rewrite rule can always be fired, once a matching is found.

In this tutorial, some basic ideas will be outlined and exemplified how graph transformation can be employed in specification and programming. In particular, some of the respective achievements of the COMPUGRAPH project will be pointed out.

In the context of Model Driven Architecture (MDA), most model transformation mechanisms aim for rigorously and unambiguously defined, fully automatic transformations. We argue that such techniques, even when fully mature, are not applicable in all cases of software development. These difficult cases would benefit from flexible and semi-automatic open transformations. We present a mechanism, so called transformational pattern system, and show how it can combine human made decisions and intentionally vague and incomplete rules to perform a transformation.

Based on a categorical semantics that has been developed for typed graph grammars we uses colimits (pushouts) to model composition and (reverse) graph grammar morphisms to describe refinements of typed graph grammars. Composition of graph grammars w.r.t. common subgrammars is shown to be compatible with the semantics, i.e. the semantics of the composed grammar is obtained as the composition of the semantics of the component grammars. Moreover, the structure of a composed grammar is preserved during a refinement step in the sense that compatible refinements of the components induce a refinement of the composition. The concepts and results are illustrated by an example.

In the paper, we propose an automated, SVG-based visualization framework for modeling languages defined by metamodeling techniques. Our framework combines XML standards with existing graph transformation and graph drawing technologies in order to provide an open, tool-independent architecture.

Consistency conditions describe basic properties of graphs as e.g. the existence or uniqueness of certain elements. A graph grammar is consistent if the start graph satisfies the consistency condition and the rules preserve this property. We propose a general construction that transforms global consistency conditions into preconditions for individual rules. A so-constructed rule is applicable to a consistent graph if and only if the derived graph is consistent, too. The relevance of this result is motivated by an example specification of a safety-critical system that is, a roundabout.

Graphical notations are already popular for the design of software, as witnessed by the success of the Uniform Modeling Languages (UML). In this paper, we advocate the use of graphs and graph transformation for programming graph-based systems. Our case study, the flattening of hierarchical statecharts, reveals that cloning, a recently proposed transformation concept, makes graph transformation rules (in the double-pushout approach) more expressive. Thus programming becomes easier, and gets along with simpler control conditions in particular.

GROOVE is a tool for the automatic generation of graph transition systems from graph grammars. In this type of tool, both memory and time performance are of prime importance. In this paper we discuss the implementation techniques used for optimising the tool in this regard, and we list possible future improvements.

Model transformation tools implemented using graph transformation techniques are often expected to provide high performance. For this reason, in the Graph Rewriting and Transformation (GReAT) language we have supported two techniques: pre-binding of selected pattern variables and explicit sequencing of transformation steps to improve the performance of the transformation engine. When applied to practical situations, we recognized three shortcomings in our approach: (1) no support for the convenient reuse of results of one rewriting step in another, distant step, (2) lack of a sorting capability for ordering the results of the pattern matching, and (3) absence of support for the distinguished merging of results of multiple pattern matches. In this paper we briefly highlight the relevant features of GReAT, describe three motivating examples that illustrate the problems, introduce our solutions: new extensions to the language, and compare the approaches to other languages.

Managing the software development and maintenance process has been identified as a great challenge for several years. Software processes are highly dynamic and can only rarely be planned completely in advance. We present an approach to software process management which is based on hierarchical nets of processes connected by data and control flow relations. Editing and execution of process nets are highly intertwined. Dynamic process nets are formally defined in PROGRES, a specification language which is based on programmed graph rewriting systems. Graph rewriting systems are a natural choice for several reasons. In particular, process nets are complicated graph structures, and editing as well as execution operations may be specified in a uniform way by graph rewrite rules. The graph rewriting system will form the foundation of a sophisticated process management system.

The GENGED concepts and environment allow for the visual definition of visual languages (VLs) and to generate VL-specific visual environments for editing and simulation. The editing features capture either syntax-directed editing and/or free-hand editing. In the latter case, a user-defined diagram has to be analyzed in order to check the correctness of the diagram. In addition, behavioral diagrams can be simulated, i.e. the behavior of situations specified by diagrams can be validated. The specification and analysis of VLs by GENGED is based on algebraic graph transformation concepts realized by the AGG system. In this article we give a brief survey on AGG and GENGED.

Proceedings of the Workshop on Graph Transformation and Visual Modelling Techniques (GT-VMT 2004), This work discusses the use of parallel graph transformation systems for (multi-formalism) modeling and simulation and their implementation in the meta-modeling tool AToM3. As an example, a simulator for Timed Transition Petri Nets (TTPN) is modeled using parallel graph transformation., This work has been partially sponsored by the SEGRAVIS network and the Spanish Ministry of Science and Technology (TIC2002-01948).

This paper presents a graph-based formalism for object-oriented class structure specifications. The formalism combines labelled graphs with partial orders, to adequately model the (single) inheritance relation among objects and the overriding relation between methods within derived classes. The semantics of system extension by inheritance and aggregation is then defined as colimits in a suitable category of object-oriented system specifications and their morphisms.

A model-to-model transformation from Dynamic Fault Trees to Stochastic Petri Nets, by means of graph transformation rules, is presented in this paper. Dynamic Fault Trees (DFT) are used for the reliability analysis of complex and large systems and represent by means of gates, how combinations or sequences of component failure events, lead to the failure of the system. DFTs need the state space solution which can be obtained by converting a DFT to a Stochastic Petri Net: this task is expressed by means of graph transformation rules, and is applied to a case of system.

When Web services are composed by linking service providers and requestors, the requestor's requirements for a "useful" service have to be matched against the service description offered by the provider. Among other things, service specifications (requirements or descriptions) may contain operation contracts specifying pre-conditions and effects of (required or provided) operations. In this paper we provide a semi-formal, UML-based notation for contracts and contract matching, as well as a formalization of these notions in terms of graph transformation. We establish the desired semantic relation between requestor and provider specifications and prove the soundness of our syntactic notion of matching w.r.t. this relation.

International audience; In this paper, we define labeled multigraphs with ports, a graph model which specifies connection points for nodes and allows multiple edges and loops. The dynamic evolution of these structures is expressed with multigraph rewrite rules and a multigraph rewriting relation. Then we encode the multigraphs and multigraph rewriting using algebraic terms and term rewriting to provide an operational semantics of the multigraph rewriting relation. This term version can be embedded in the rewriting calculus, thus defining for labeled multigraph transformations a high-level pattern calculus, called rho-mg calculus.

Graphs may be used as representations of system states in operational semantics and model checking; in the latter context, they are being investigated as an alternative to bit vectors. The corresponding transitions are obtained as derivations from graph production rules.In this paper we propose an abstraction technique in this framework: the state graphs are contracted by collecting nodes that are sufficiently similar (resulting in smaller states and a finite state space) and the application of the graph production rules is lifted to this abstract level. Since graph abstractions and rule applications can all be computed completely automatically, we believe that this can be the core of a practically feasible technique for software model checking.

Graph grammars may be used as specification technique for different kinds of systems, specially in situations in which states are complex structures that can be adequately modeled as graphs (possibly with an attribute data part) and in which the behavior involves a large amount of parallelism and can be described as reactions to stimuli that can be observed in the state of the system. The verification of properties of such systems is a difficult task due to many aspects: the systems in many situations involve an infinite number of states; states themselves are complex and large; there are a number of different computation possibilities due to the fact that rule applications may occur in parallel. There are already some approaches to verification of graph grammars based on model checking, but in these cases only finite state systems can be analyzed. Other approaches propose over- and/or under-approximations of the state space, but in this case it is not possible to check arbitrary properties. This work proposes a relational and logical approach to graph grammars that allows formal verification of systems using mathematical induction. We use relational structures to define graph grammars and first-order logic to model graph transformations. This approach allows proving properties of systems with infinite state spaces. In this paper we first consider the case of simple (typed) graphs, and then we extend the approach to the non-trivial case of attributed graphs, that are graphs in which values are associated to vertices. Attributed graph grammars are very interesting from a practical point of view, since it is possible to use variables and terms when specifying the behavior expressed by rules. These values (or terms) come from algebras specified as abstract data types. The use of attributed graphs gives the specifier a language that is more suitable for specification, merging the advantages of the graphical representation with the standard representation of classical data types. We show that attributes can be smoothly integrated in our representation of graph grammars, giving rise to a framework to reason about attributed graph grammars.

Gene assembly in ciliates is an extremely involved DNA transformation process, which transforms a nucleus, the micronucleus, to another functionally different nucleus, the macronucleus. In this paper we characterize which loop recombination operations (one of the three types of molecular operations that accomplish gene assembly) can possibly be applied in the transformation of a given gene from its micronuclear form to its macronuclear form. We also characterize in which order these loop recombination operations are applicable. This is done in the abstract and more general setting of so-called legal strings., Comment: 22 pages, 14 figures