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
    ------------------------------------------------------