Abstracts of talks at the Aussois IFIP WG1.3 meeting

Abstracts of talks at the Aussois IFIP WG1.3 meeting (January 6-9th, 2011)

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:

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:

9 - Bartek Klin, University of Cambridge and University of Warsaw
title
Abstract:

10 - Till Mossakowski,
Change management for the heterogeneous tool set
Abstract: