Abstracts of talks at the Aussois IFIP WG1.3 meeting

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

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, Universitaet Augsburg, slides, paper
A heterogeneous approach to service oriented system specification
[Joint work with] Grzegorz Marczynski, Martin Wirsing, and Artur Zawlocki
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 "local" logic and where the specification of their interactions is separately described in a "global" 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
[Joint work with] Sergey Goncharov
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, University of Leicester slides, and paper
An Interface Theory for Service-Oriented Design
[Joint work with] Antonia Lopes
Abstract:
We revisit the notions of interface and component algebra proposed by de Alfaro and Henzinger for component-based design and put forward elements of a corresponding interface theory for service-oriented design. We view services as a layer that can be added over a component infrastructure and propose a notion of service interface for a component algebra that is an asynchronous version of relational nets adapted to SCA (the Service Component Architecture developed by the Open Service-Oriented Architecture collaboration).

More information is available at http://www.cs.le.ac.uk/srml/

5 - Dominique Duval, University Joseph Fourier of Grenoble slides
Decorated specifications for states and exceptions
[Joint work with] Jean-Guillaume Dumas, Laurent Fousse and Jean-Claude Reynaud
Abstract:
This talk is about the semantics of programming languages, more precisely the semantics of two computational effects: states and exceptions.
Effects can be formalized thanks to monads [Moggi 1989] or Lawvere theories [Plotkin Power 2001], however in this talk we rather use decorated specifications [Duval Lair Reynaud 2003].
First we present decorated specifications as a generalization of monads and we give a motivating object-oriented example. Then we build a decorated specification for states and one for exceptions.
This yields a new point of view on states, a new categorical formalization of exceptions with handling, and an unexpected duality between states and exceptions.

6 - Pawel Sobocinski, University of Southampton slides and paper
Deriving LTS (structural labelled transition systems from reduction rules)
[Joint work with] Julian Rathke
Abstract:
Behavioural equivalences of various concurrent calculi di\ufb00er signi\ufb01cantly because the properties which can be observed through interaction depend heavily upon their mode of communication. A typical approach to describing the semantics of communicating processes is to provide a labelled transition system (LTS) which captures the interaction potential of the individual processes within a larger system.

In many cases, a natural rendering of this lts leads to too \ufb01ne a semantics as unobservability of certain communications is not accounted for. We propose that a standard approach to augmenting LTSs allows morally unobservable communications to actually be modelled as unobservables in the semantics. This approach derives from a rule initially given by Honda and Tokoro to account for unobservability of reception in the asynchronous pi-calculus. We will examine the implications of adding such rules to lts with respect to the proving behavioural equivalences for various synchronisation mechanisms.

7 - David Chemouil, Onera, Toulouse slides
Requirements engineering and multi-agent temporal logic
[Joint work with] Julien Brunel, Christophe Chareton
Abstract:
We report on an on-going project regarding the definition of a formal language for requirements engineering (RE). This language can be seen as a combination of the formal part of the KAOS language, but considering agents as first-class objects as in the Tropos approach. To consider both goals and agents, the semantics is based upon the multi-agent temporal logic ATL. This apporach enables to consider formally the question of the assignment of actors (available or pre-existing agents) to roles (agents needed to fulfill the goals).

8 - Alexander Knapp, Universitaet Augsburg, slides
The Java memory model: operationally, axiomatically, denotationally
[Joint work with] Pietro Cenciarelli, Eleonora Sibilio
Abstract:
A semantics to a small fragment of Java capturing the new memory model (JMM) described in the Language Specification is given by combining operational, denotational and axiomatic techniques in a novel semantic framework. The operational steps (specified in the form of SOS) construct denotational models (stable configuration structures) and are constrained by the axioms of a configuration theory. The semantics is proven correct with respect to the Language Specification and shown to capture many common examples in the JMM literature.

9 - Andrzej Tarlecki, University of Warsaw & Polish Academy of Science slides
Another old story: compositional property-oriented semantics for structured specifications
Abstract:
Working in an arbitrary institution, we discuss property-oriented semantics of specifications built using some collection of specification-building operations. As a typical example we consider the structured specifications built from flat specifications using union, translation and hiding. For such specifications we have the standard compositional proof system, which determines the standard property-oriented semantics assigning a theory to each structured specification. It is not complete (unless the underlying logic has interpolation and enjoys some other technical properties) but otherwise it is "as good as can be expected". In particular, it is sound, monotone (and hence compositional) and one-step complete. The last property means that the semantics (and the corresponding proof system) allows us to deduce all true consequences for specifications built by applying any specification-building operation to argument specifications, assuming that there is no discrepancy between the classes of models of the argument specifications and the classes of models of their respective property-oriented meanings. This is a strong property which was believed to ensure that the semantics is "as strong as possible" without loosing soundness or compositionality. We question this claim and show that it holds assuming in addition that the semantics considered are not "absent-minded", i.e., do not loose axioms of flat specifications. We sketch an example to show that by excluding deduction of some axioms in flat specifications we may offer a stronger rule for natural specification-building operation so that for some specifications the resulting semantics is stronger than the standard one.

10 - Till Mossakowski, DFKI Bremen slides
Change management for the heterogeneous tool set
[Joint work with] Serge Autexier, Dominique Dietrich, and Dieter Hutter
Abstract:
The error-prone process of formal specification and verification of large systems requires an efficient, evolutionary formal development approach. Development graphs have been designed to support such an approach. They can formally represent the actual state of a software development comprising specification and verification work in a structured way and assist the user in her evolutionary development by the incorporated change management support. In this paper we extend this work with respect to heterogeneous development graphs allowing one to make use of different institutions, i.e. logics, for specifying and verifying large developments. We also push forward the idea of stringent locality of definitions by introducing pre-signatures and pre-signature morphisms, which allow us to build up signatures in an incremental and parametric way.

11 - Bartek Klin, University of Cambridge and University of Warsaw slides
Nominal automata
[Joint work with] Mikolaj Bojanczyk, Slawomir Lasota
Abstract:
First I will show how a simple categorical understanding of detereministic automata in the spirit of Arbib and Manes, when instantiated in the category of nominal sets as stued by Gabbay and Pitts, yields a useful model of finite computation on infinite alpabets, closely related to HD-automata of Pistore and others, and enjoying better properties then Finite Memory Automata of Francez and Kaminski. These are then generalized to cater for alphabets with structure (such as an order or a graph) that can be checked upon by automata. In the process, the theory of nominal sets needs to be generalized to arbitrary groups of permutations rather than symmetric groups. A particularly well behaved class of alphabets arises from the model-theoretic study of Fraisse limits.

1 - Dirk Pattinson, Imperial College, London slides
Fun with Henry
Abstract:
In this talk, we are using the example of Henry VIII's court to explain basic principles of logic-based knowledge representation in a general (coalgebraic) framework. In a nutshell, knowledge is represented by formulas, and automated reasoning then accomplishes the task of hypothesis testing. We discuss the general setup using probabilistic logics as a guiding example and then showcase the feasibility of our approach by demonstrating a prototypical implementation.