| Abstracts: |
Conditional
Reactive Systems
Barbara
König
Reactive
Systems were introduced by Leifer and Milner. They provide a general
categorical setting for modelling abstract rewriting: graph
transformation systems, process calculi and also Petri nets can be seen as special cases of
reactive systems.
In
this talk the notion of nested application conditions will be lifted
from graph transformation systems to the setting of reactive
systems. This serves two purposes: first, we enrich the
formalism
of reactive systems by adding application conditions for
rules; second, it turns out that some constructions for
graph transformation systems (such as computing weakest
preconditions and strongest postconditions and showing local
confluence by means of critical pair analysis) can be done
elegantly in the more general setting.
Transfer
of
Local Confluence and Termination between
Petri Net and Graph Transformation Systems Based on M-Functors
Maria
Maximova, Hartmut Ehrig, Claudia Ermel
Recently,
a formal relationship between Petri net and graph transformation
systems has been established using the new framework of M-functors F:
(C1,M1) -> (C2,M2) between M-adhesive categories. This new
approach
allows us to translate transformations in (C1,M1) into corresponding
transformations in (C2,M2) and, vice versa, to create transformations
in (C1,M1) from those in (C2,M2). In this paper, we extend this
framework to the transfer of local confluence, termination and
functional behavior. In particular, we are able to create these
properties for transformations in (C1,M1) from corresponding properties
of transformations in (C2,M2), where (C1,M1) are Petri nets with
individual tokens and (C2,M2) typed attributed graphs. This allows us
to apply the well-known critical pair analysis for typed attributed
graph transformations supported by the AGG-tool
in order to analyze these properties for Petri net transformations.
Process
Evolution based on Transformation of Algebraic
High-Level Nets with Applications to Communication Platforms
Karsten
Gabriel
Algebraic High-Level (AHL) nets
are a well-known modelling technique based on Petri nets with algebraic
data types, which allows to model the communication structure and the
data flow within one modelling framework. Transformations of AHL-nets
-- inspired by the theory of graph transformations -- allow in addition
to modify the communication structure. Moreover, high-level processes
of AHL-nets capture the concurrent semantics of AHL-nets in an adequate
way. Altogether we obtain a powerful integrated formal specification
technique to model and analyse all kinds of communication based
systems, especially different kinds of communication
platforms.
In this paper we show how to model the evolution of
communication platforms and scenarios based on transformations of
Algebraic High-Level Nets and Processes. All constructions and results
are illustrated by a running example showing the evolution of Apache
Wave platforms and scenarios. The evolution of platforms is modelled by
the transformation of AHL-nets and that of scenarios by the
transformation of AHL-net processes.
Our main result is a
construction for the evolution of AHL-processes based on the evolution
of the corresponding AHL-net. This result can be used to transform
scenarios in a communication platform according to the evolution of
possibly multiple actions of the platform.
On Modelling
Communication in Ubiquitous Computing
Systems using Algebraic Higher Order Nets
Susann
Gottmann,
Nico Nachtigall and Kathrin Hoffmann
Ubiquitous computing systems
(UCSs) are designed to participate almost imperceptibly in everyday
life. To ensure a solid operation, a UCS heavily relies on a reliable
and efficient communication between its distributed computing
components where components can join and leave the system at any time.
In order to guarantee high quality systems, the use of models is
inevitable especially at an early stage of the development process
where models are the only possibility to address a system which does
not yet exist in reality. Petri nets and graph transformation systems
are established, theoretically well-founded concepts for modelling and
analysing complex systems.This paper presents a formal approach for
modelling core aspects of the communication in UCSs by using algebraic
higher-order nets with individual tokens and graph transformation. In
contrast to a wide range of other modelling techniques, this approach
is suitable to cover the different aspects of communication in an
integrative form and enables the analysis of specific properties. The
approach and its suitability are illustrated based on a running
example. The feasibility of embedding the approach in a broader context
of modelling is demonstrated in applying it to a real world system: the
Living Place Project.
Optimization
in Graph
Transformation Systems with Time Using Petri Net Based Techniques
Szilvia
Varró-Gyapay
Extra-functional properties of
IT systems have to be analyzed and subsequently optimized carefully
during the design phase in order to assure a proper quality of service
and decrease operational costs. Several verification and validation
methods are known to check the correctness of the system services,
while optimization may serve to reach boundaries thus minimizing costs
or duration of operating the system. However, the combination of the
best practices of the two fields according to
the purpose of
the analysis is a challenging question. In a previous paper, we showed
how such a problem can be formalized and solved when the evolution of
the system is captured by graph transformation systems (GTS) with cost
parameters attached to each graph transformation rule denoting the cost
of firing the rule. This
technique is adapted in the current paper to deliver a time-optimal
trajectory in a GTS with time. While the cost of a GT rule sequence
always equals to the sum of the cost of the involved GT rules, the
concurrent application of GT rules may reduce the minimal duration of a
GT rule sequence, which is a major conceptual difference concerning
optimization.
Abstract
Interleaving Semantics for Reconfigurable
Petri Nets
Julia
Padberg
Reconfigurable Petri nets are
Petri nets together with rules for the dynamic change of the nets. We
employ them for the formal modeling in the context of the Living Place
Hamburg, a smart home that is an urban apartment serving as a
laboratory for investigating different areas of ambient intelligence.
The
interaction of the resident and the smart home is modeled using
informal descriptions of scenarios. These scenarios provide the
resident's procedures together with the smart home's support.
The case study
using reconfigurable Petri nets for modeling these scenarios has led to
necessary extensions of the theory and has clearly shown the need for
an interleaving semantics of the reconfigurable Petri nets. Scenarios
are then given by nets, namely decorated place/transition nets that can
be adapted to the evolving subgoals by applying rules that change the
nets and hence the behavior of the smart home.
Decorated
place/transition nets are annotated P/T nets with additional transition
labels that may change when the transition is fired. To obtain
reconfigurable Petri nets based on these decorated P/T nets we prove
that they give rise to a M-adhesive HLR category.
The
abstract interleaving semantics we introduce is a graph with nodes that
consist of an isomorphism class of the net structure and an isomorphism
class of the actual marking. Arcs between these node represent
computation steps being either a transition firing or a direct
transformation.
|
