On the Occasion of
Hartmut Ehrig’s 65th Birthday,
TU Berlin, February
11-12, 2010
Authors: Roberto Bruni, Andrea Corradini and Ugo Montanari
Title: Modelling a Service and Session Calculus
with Hierarchical Graph Transformation
Abstract: Graph transformation techniques have been applied successfully
to the modelling of process calculi, for example for equipping them with a truly
concurrent semantics. Recently, there has been an increasing interest towards
hierarchical structures both at the level of graph-based models, in order to
represent explicitly the interplay between linking and containment (like in
Milner's bigraphs), and at the level of process calculi, in order to deal with
several logical notions of scoping (ambients, sessions, and transactions, among
others). In this paper we show how to encode a sophisticated calculus of
services and nested sessions by exploiting a suitable flavour of hierarchical
graphs. For the encoding of the processes of this calculus we benefit
from a recently proposed algebra of graphs with nesting.
Title:
Symbolic Attributed Graphs for Attributed Graph Transformation
Abstract: In this paper we present a new approach
to deal with attributed graphs and attributed graph transformation. This
approach is based on working with what we call symbolic graphs, which are
graphs labelled with variables together with a formula that constrains the
possible values that we may assigned to these variables. In particular, in this
paper we will compare in detail this new approach with the standard approaches
to attributed graph transformation.
Author: Claudia
Ermel and Karsten Ehrig
Title: Graph Modelling and Transformations
Abstract: Graphs are one of the key concepts for
modelling. Since the early days of mankind, graphs are used to depict the
relationship between two or more entities.
The fundamental notions behind graph models nowadays have been captured
by mathematical terms which play a central role in theoretical computer science
today.
Real
world systems evolve, and hence graph system models need to model evolution as
well. Algebraic graph transformation
techniques have been developed as a formal basis for visual language
definition, system behaviour modelling and model transformation.
In
this paper, we focus on the role of graphs and graph transformation for three
practical application areas from software system development: 1) visual language modelling, 2) automotive systems, and 3) public transportation.
We
present the typical problems in these areas and investigate how the respective
systems are modelled by graphs and graph transformation. In particular, we are interested in the
usefulness of theoretical graph theory and graph transformation results in
order to solve the typical problems.
Finally,
we characterize useful graph transformation concepts, results and tool features
which are still missing in practice to solve these problems in a satisfactory
way.
Author: Francesco Parisi-Presicce and Paolo Bottoni
Title A Termination Criterion for Graph Transformation Systems with NACs
Abstract: Termination of graph rewriting is in
general undecidable, but it is possible to prove it for specific systems by
checking for sufficient conditions. In
the presence of rules with negative application conditions, the difficulties
increase. In this paper we propose a
different approach to the identification of a (sufficient) criterion for
termination based on the construction of a labeled transition system whose
states represent overlaps between the negative application condition and the
right hand side that can give rise to cycles.
Author: Kathrin Hoffmann, Julia Padberg and Tony Modica
Title: Formal Modeling and Analysis of Flexible Processes Using Reconfigurable Systems
Abstract: In mobile and adaptive communication
systems, communicating entities, actors, can transmit content, which is
contextually interpreted. Actors may join, move in or leave so-called
communication spaces, where the actors' preferences, access rights and roles
are respected
and
define a temporary set of communicating partners and a context of
interpretation for communicated data. In our research project "Formal
modeling and analysis of flexible processes in Communication Based
Systems", we have proposed an appropriate integration of Petri
nets
and Petri net transformation rules based on graph transformation by
reconfigurable systems.
In
this paper we give a characterization of main requirements for flexible
processes in communication based systems in order to review the formal notions
of reconfigurable systems. The main part presents a case study in the area of
communication platforms and demonstrates the advantages of our approach which
allows the dynamic adaption of processes in such environments. In this context
we also discuss the main results achieved for reconfigurable systems and
outline some interesting aspects of future work.
Authors: Tiziana Margaria and
Bernhard Steffen
Title:
Second-Order Value Numbering
Abstract:
We present second-order value
numbering, a new optimization method for
suppressing redundancy, in a version tailored to the application for optimizing the decision procedure of
jMosel, a verification toolset for
monadic second-order logic on strings (M2L(Str)).
The
method extends the well-known concept of value numbering to consider not merely values, but semantics
transformers, realized as
transformations on directed acyclic graphs, that can be efficiently precomputed and help to avoid
redundancy at the 2nd-order level.
Since decision procedures for M2L are
non-elementary, an optimization method like this can have a great impact on the
execution time, even though our decision
procedure comprises the analysis and optimization time for second-order value numbering. This is
illustrated considering a parametric family of hardware circuits, where we
observed a performance gain by a factor of 3.
This
result is surprising, because the design of these circuits already exploits
structural similarity.
Authors: Simone Costa,
Fabiane Dillenburg, Fernando Dotti and Leila
Ribeiro
Title: Theorem Proving Graph Grammars using Event-B
Abstract: 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. In this work, we propose to use the Event-B formal method and its
theorem proving tools to analyze graph grammars. We show that a graph grammar
can be translated into an Event-B specification preserving its semantics, such
that one can use several theorem provers available for Event-B (for instance,
through the Rodin platform) to analyze the reachable states of the original
graph grammar. The translation is based on a relational definition of graph
grammars that was shown to be equivalent to the Single-Pushout approach to
graph grammars.
Authors: Annegret Habel and Hendrik Radke
Title:
Expressiveness of Graph Conditions with Variables
Abstract: Graph conditions are most important for
graph transformation systems and graph programs in a large variety of
application areas. Nevertheless, non-local graph properties in the sense of
[Gaifman 82] like “there exists a path”, “the graph is connected”, and “the
graph is cycle-free” are not expressible by finite graph conditions. In this
paper, we generalize the notion of finite graph conditions, expressively
equivalent to first-order formulas on graphs, to finite graph conditions with
variables where the variables are place holders for graphs generated by a
hyperedge replacement system. We show that graphs with variables and
replacement morphisms form a weak adhesive HLR category. We investigate the
expressive power of graph conditions with variables and show that finite graph
conditions with variables and monadic second-order graph formulas are
incomparable.
Authors: Reiko Heckel and Mayur Bapodra
Title:
From Graph Transformations
to Differential Equations
Abstract: In a variety of disciplines models are
created to predict or explain quantitative measurements involving time in
dynamic systems. Examples include the concentration of a chemical substance
produced within a given period of time, the growth over time of the size of a
population of individuals, the time taken to recover from a communication
breakdown in a P2P network, etc.
The models of these measurements arise
from are often discrete and structural in nature. Adding information on the
time and/or probability of any actions performed, quantitative models can be
derived. In the first example above, commonly referred to as Kinetic Analysis
of Chemical Reactions, a system of differential equations describing the
evolution of concentrations is extracted from specifications of individual
chemical reactions augmented with reaction rates.
Recently, this construction has
inspired approaches based on stochastic process specification techniques aiming
to extract a continuous, quantitative model of system from a discrete,
structural one. This paper describes a
methodology for such an extraction based on a model of chemical reactions as stochastic graph
transformations.
Graph transformations have a particular
appeal as s model of chemistry because they allow representing the reactivity
within a system in a local molecular context. Start graphs and rules bear a
conceptual similarity to structural formulae used in Chemistry, thereby
reducing the semantic gap.
The methodology for extracting
ordinary differential equations from stochastic graph transformation systems is
based on a variant of the construction of critical pairs and has been validated
using the AGG tool for a simple reaction of unimolecular nucleophilic
substitution (SN1).
After
presenting the general method and its application, we discuss its limitations
as well as potential for wider use in other areas.
Title: Reaction Systems - a formal framework for biochemical reactions
Abstract: The functioning of a living cell
consists of a huge number of individual reactions that interact with each
other. These reactions are regulated, and the two main regulation mechanisms
are facilitation/acceleration and inhibition/retardation. The interaction
between individual biochemical reactions takes place through their influence on
each other, and this influence happens through the two mechanisms mentioned
above.
In our lecture we present a formal
framework for the investigation of biochemical reactions - it is based on
reaction systems. We motivate them by explicitly stating a number of
assumptions/axioms that (we believe) hold for a great number of biochemical
reactions - we point out that these assumptions are very different from the
ones underlying traditional models of computation, such as, e.g., Petri nets.
We illustrate the basic notions by both biology and computer science oriented
examples. We demonstrate some basic properties of reaction systems, and
demonstrate how to capture and analyze in our framework some biochemistry
related notions.
The lecture is of a tutorial
character and self-contained. In particular, no knowledge of biochemistry is
required.
Authors: Björn Bartels, Sabine
Glesner and Thomas Göthel
Title: Model Transformations to Mitigate the Semantic Gap in Embedded
Systems
Verification
Abstract: Embedded
systems are often employed in safety-critical areas. Their functional correctness is therefore
extremely important in order not to endanger human lives or risk high financial
losses. The verification of the software employed in these systems is an open
problem
which is particularly hard as many systems are concurrent, underlie real-time
constraints and are implemented in higher programming languages as e.g. C++.
In this talk, I present results from the
VATES project which addresses the problem of verifying embedded software by
employing a novel combination of methods that are well-established on the level
of declarative models, in particular process-algebraic specifications, as well
as of methods that work especially well on the level of the actually executed
code. In the VATES approach, we start from code given in an intermediate
compiler format. From this code, we extract a model in the form of a
process-algebraic system description formulated in Timed CSP. For this CSP
description, we prove that the original implementation code is a refinement.
This proof enables us to conduct
correctness
proofs on the higher abstraction level of Timed CSP as well as on the lower
intermediate code level. In my talk I show that this approach has the potential
to seamlessly integrate modeling, implementation, transformation and
verification stages of embedded system development.
Authors: Frank Hermann, Barbara König and Matthias Hülsbusch
Title: Specification and Verification of Model Transformations
Abstract:
Model transformations are a key concept within
model driven development and there is an enormous need for suitable formal
analysis techniques for model transformations, in particular with respect
to behavioural equivalence of source models and their corresponding target
models.
For this reason, we discuss
the general challenges that arise for the specification and verification of
model transformations and present suitable formal techniques that are based on
graph transformation. In this context, triple graph grammars show
many benefits for the specification process, e.g. modelers can work on
an intuitive level of abstraction and there are formal results
for syntactical correctness, completeness and efficient execution.
In order to verify model transformations with respect to behavioural
equivalence we apply well-studied techniques based on the double pushout
approach with borrowed context, for which the model transformations specified
by triple graph transformation rules are flattened to plain (in-situ) graph
transformation rules.
The potential and adequateness
of the presented techniques are demonstrated by an intuitive example, for which
we show the correctness of the model transformation with respect to
bisimilarity of source and target models.
Authors: Hans-Jörg
Kreowski, Sabine Kuske, and Caro von Totth
Title: Stepping from Graph Transformation Units to Model Transformation Units
Abstract:
Graph transformation units model binary
relations between initial and terminal graphs by means of regulated rule
applications. If the initial and terminal graphs are visual models of
some kind like UML diagrams,
then graph transformation units model model transformations.
In the
present paper, this basic observation is elaborated by
(1)
considering not only graphs, but also tuples and sets of graphs
as models,
(2)
introducing sequential and parallel
compositions of model transformations to build up complex
model transformations from simple ones, and
(3)
pointing out possible notions of correctness.
Authors:
Gregor Engels, Christian Soltenborn
Title: Test-driven Language Derivation with Graph Transformation-based Dynamic
Meta Modeling
Abstract: Deriving a new language L_B from an
already existing one L_A is a typical task in domain-specific language engineering.
Here, besides adjusting L_A's syntax, the language engineer has to modify the
semantics of L_A to derive L_B’s semantics. Particularly in case of behavioral
modeling languages, this is a difficult and error-prone task, as changing the
behavior of language elements or adding behavior for new elements might have
undesired side effects.
Therefore, we propose
a test-driven language derivation process. In a first step, the language
engineer creates example models containing the changed or newly added elements
in different contexts. For each of these models, the language engineer also
precisely describes the expected behavior. The second step consists of
transforming each example model and its description of behavior into an
executable test case. These test cases are used when deriving the actual
semantics of L_B – at any time, the language engineer can run the tests to
verify whether her specification indeed produces the desired behavior.
In this paper, we illustrate the
approach using our graph transformation-based semantics specification technique
Dynamic Meta Modeling (DMM). This is once more an example, where the graph
transformation approach shows its strengths and appropriateness to support
software engineering tasks as, e.g.,
model transformations, software specifications or tool development.
Author: Hartmut Ehrig
Title: From Single Formal Specifications to Certified Integrated Visual
Modelling Techniques
and Environments
Abstract: According
to the title of the panel discussion "Software System Modelling : Past,
Presence, Future " we discuss the state of the art and role of formal
methods in different periods. In the Past (1970-1990) single formal
specification techniques have been developed with little impact on practical
software development. In the Presence (1990- 2010) integrated and visual
modeling techniques have gained more and more importance. For the Future
(2010-2020) we try to sketch the idea of a "Certified Integrated Visual
Modelling Technique and Environment" based on an integration of
"Graph Theory, Graph Transformation and Petri Net Theory", short
"Dynamic Graph and Net Theory".
Author: Michael Löwe
Title: Formal Methods and Agile Development
Abstract: There have been two major trends in software
engineering for the last decade: (1) raising the level of abstraction for
software systems design (even further) and (2) providing (more
sophisticated) methods for agile development. The first trend is connected with
catch words like “Model-driven Development”, “Service-Oriented Architectures”,
and “Business Process Modelling”. The second trend is characterized by concepts
like “Software Refactoring”, “Test-First”, “Extreme Programming” or “Dynamic
Systems Development”.
In the first area, formal methods,
especially graph transformations, have provided precise semantics for model
specifications and transformation concepts from abstract to concrete system
descriptions including correctness notions for static as well as dynamic models
(data structures respectively process models).
In the second area, formal methods have not been applied that much, yet.
At first glance, agility and formal preciseness do not go together well.
We argue in this position paper that this
first impression is wrong and that there is great potential for graph
transformation techniques in agile contexts. The rapid redesign of software
systems is not chaotic. It is a continuous process that introduces changes or
removes system structure, mostly without changing the external behaviour of the
system. Hence, what is needed is a catalogue of evolution patterns that
preserve system semantics.
Practical applicability, however,
requires that we do not restrict ourselves to the level of static and dynamic
models only. We also have to take into account that the models are populated,
which means that there is (typically terra-bytes of) data typed in the static
model and (lots of) running processes typed in the dynamic model. Thus,
evolution patterns have to provide canonically induced and correct migrations
on the instance level as well. Therefore,
formal methods that support agile development shall provide (1) suitable
semantics for “populated” systems, (2) formal concepts for refactorisations and
induced migrations, (3) a notion of correctness for such
factorisations/migrations, and (4) a catalogue of practically useful and
correct patterns. The existing body of concepts and results within the research
area of “Graph Transformation” seems to be a good starting point for this
programme.
Author: Bernd Mahr
Title: Software Systems Modelling creates complex interconnections of models
Abstract: Modelling of software systems is on
the one side rooted in requirements which concern properties and features of
the intended systems application and use, and is on the other side depending on
the given properties and constraints of the intended systems implementation,
technical realization and social and technical environments. All, application
and use of the intended system, as well as its implementation, technical
realization and environments are at the time of the systems modelling available
only as models themselves. Moreover, also in the processes of modelling,
specification and implementation of the intended system use is being made of
models, not only implicitly in the formalisms and languages applied, but also
explicitly in the design patterns used, and in the basic structures of the
systems architecture and processing elements. The modelling of software systems
is therefore a task in which a complex interconnection of models is being
created.
Following the author’s conceptualization
of a model as a particular kind of epistemic pattern, and of model combinations
which allow to describing and analysing structures of model interconnections,
the question is raised if there are advantages in a careful analysis and
evaluation of the structure and content of the complex model interconnections
as they appear in the practice of systems modelling. In the long run, it could
be the case that such analysis and evaluation does lead to a new kind of a
theory for the modelling of software systems. The theory would be based on a
reference for model interconnections derived from best practice of software
systems modelling.
Author: Gabriele Taentzer
Title: What Graph Transformations can do for Model Transformations
Abstract: Domain-specific
modeling and model transformations play central roles in model-driven software
development. Most domain-specific modeling languages are visual ones.
Considering the underlying structures of visual models they can be defined very
naturally by graphs. For the definition of visual modeling languages as well as
for different kinds of model manipulations an adequate transformation approach
is needed. Graph transformation is a formalism which offers structure and type
consistent model transformations by defining rule-based transformations of
typed graphs. Furthermore, graph transformation supports the visual notation of
transformation rules for the description of model patterns that are required,
forbidden or newly created.
The theory of algebraic graph
transformation offers concepts and results which can be advantageously used to
show important properties of model transformations. These are e.g. the
guaranteed type consistency of transformation results, the functional behaviour
of model transformations as well as finding conflicts and dependencies between
transformation steps.
Graph transformation seems
to be a promising formal basis also for newly arising model transformation
topics such as model versioning and n-to-m model transformations.