Abstracts of talks at the Aussois IFIP WG1.3 meeting
Abstracts of talks at the Aussois IFIP WG1.3 meeting (January 6-9th, 2011)
== Thursday January 6th, 2011 - 8h30 --
- 1 - Reiko Heckel, University of Leicester
slides
Parallelism and Concurrency of Stochastic Graph Transformations
[Joint work with] Hartmut Ehrig, Ulrike Golas, Frank Hermann
Abstract:
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 simulations. In this talk we develop the basic theory of stochastic graph transformation, including generalisations of the Local Church-Rosser, Parallelism and Concurrency Theorems and their application to computing the completion time of a concurrent process.
------------------------------------------------------
- 2 - Alexander Knapp, University
slides
A heterogeneous approach to service oriented system specification
[Joint work with] Grzegorz Marczynski, Martin Wirsing, and Artur Zaw\u0142ocki
Abstract:
Service-oriented architecture (SOA) is a relatively new approach to software system development. It divides system functionality to independent, loosely coupled, interoperable services. In this paper we propose a new heterogeneous specification approach for SOA systems where a heterogeneous structured specification consists of a number of specifications of individual services written in a \u201clocal\u201d logic and where the specification of their interactions is separately described in a \u201cglobal\u201d logic. A main feature of our global logic is the possibility of describing the dynamic change of service communications over time. Our approach is based on the theory of institutions: we show that both logics form institutions and that these institutions are connected by an institution comorphism. We illustrate our approach by a simple scenario of an e-university management system and show the power of the heterogeneous specification approach by a compositional refinement of the scenario.
------------------------------------------------------
- 3 - Lutz Schroeder, DFKI Bremen
slides
Tensoring unranked effects
Abstract:
Both in semantic theory and in programming practice, algebraic
concepts such as monads or, essentially equivalently, (large)
Lawvere theories are a well-established tool for modelling generic
side-effects. An important issue in this context are combination
mechanisms for such algebraic effects, which allow for the modular
design of programming languages and verification logics. The most
basic combination operators are sum and tensor: while the sum of
effects is just their non-interacting union, the tensor imposes
commutation of effects. However, for effects with unbounded arity,
such as continuations or unbounded non-determinism, it is not a
priori clear whether these combinations actually exist in all
cases. Here, we introduce the class of uniform effects, which
includes unbounded non-determinism and continuations, and prove that
the tensor does always exist if one of the component effects is
uniform, thus in particular improving on previous results on
tensoring with continuations. We then treat the case of (unbounded)
non-determinism in more detail, and give an order-theoretic
characterization of effects for which tensoring with non-determinism
is conservative, thus enabling non-deterministic arguments for
deterministic programs such as a generic version of the
Fisher-Ladner encoding of control operators.
------------------------------------------------------
- 4 - Jose Fiadeiro
An Interface Theory for Service-Oriented Design
Abstract:
------------------------------------------------------
== Friday January 7th, 2011 - 8h30 --
- 5 - Dominique Duval
Decorated specifications for states and exceptions
Abstract:
------------------------------------------------------
- 6 - Pawel Sobocinski,
DSSE, ECS, University of Southampton
Deriving structural labelled transition systems from reduction rules
Abstract:
------------------------------------------------------
- 7 - David Chemouil, Onera
Requirements engineering and multi-agent temporal logic
Abstract:
------------------------------------------------------
- 8 - Alexander Knapp, University
The Java memory model: operationally, axiomatically, denotationally
Abstract:
------------------------------------------------------
== Saturday January 8th, 2011 - 8h30 --
- 9 - Bartek Klin,
University of Cambridge and University of Warsaw
title
Abstract:
------------------------------------------------------
- 10 - Till Mossakowski,
Change management for the heterogeneous tool set
Abstract:
------------------------------------------------------
- 11 - Andrzej Tarlecki,
University of Warsaw
title
Abstract:
------------------------------------------------------
== Sunday, January 9th, 2011
------------------------------------------------------