Abstracts

We present a novel coalgebraic logic for deterministic Mealy machines that is sound, complete and expressive w.r.t. bisimulation. Every finite Mealy machine corresponds to a finite formula in the language. For the converse, we give a compositional synthesis algorithm which transforms every formula into a finite Mealy machine whose behaviour is exactly the set of causal functions satisfying the formula.

Cobases coalgebraically (Clemens Kupke)

t.b.a

A Relational Model for Confined Separation Logic (J. N. Oliveira)

Confined separation logic is a new extension to separation logic designed to deal with problems involving dangling references within shared mutable structures. In particular, it allows for reasoning about confinement in object-oriented programs. In this paper, we discuss the semantics of such an extension by defining a relational model for the overall logic, parametric on the shapes of both the store and the heap. This model provides a simple and elegant interpretation of the new confinement connectives and helps in seeking for duals. A number of properties of this logic are proved calculationally.

Generating connector laws (Dave Clarke)

This talk describes an approach to finding laws for reasoning
about stateful connectors such as those found in Reo.

Towards Distributed Reo (Jose Proenca)
 

Reo is an exogenous coordination language based on a calculus of
connector composition. Complex connectors are built by composing simpler
connectors, starting with a user-defined set of atomic connectors as
primitives. Various semantic models exist to formalize Reo, each serving
a different purpose. In this work we mainly focus on formal models
suitable for deriving a distributed implementation.

For our implementation platform, we assume a distributed environment
where each (distributed) element knows about its own neighbors only. We
propose an executable model to explicitly deal with distribution
issues that is very close to this implementation layer. We present how
the design and the implementation can be seen in a common architecture.
Finally, we describe how synchronous constrains, imposed by Reo
semantics, can be dealt with using asynchronous messages.  

Eclipse Coordination Tools(Christian Koehler)

The Eclipse Coordination Tools project aims at integrating a number of existing development tools for Reo in the well-known Eclipse IDE. The tied integration of these tools allows to rapid prototype Reo connectors with 
a graphical editor, simulate and model check these connectors and finally generate highly customized runnable code.

In this talk I will give an overview of the current status of the tools, followed by a short demo.





Bi-directional Transformations @ Uminho (Alcino Cunha)

t.b.a

Putting interactors together (Luis Barbosa)

Although presented with a variety of 'flavours', the notion of an interactor, as an abstract characterisation of an interactive component, is well-known among formal modelling techniques for interactive systems. This talk discusses how (Reo-like) exogenous coordination schemes can be applied in this domain, replacing the traditional, hierarchical, 'tree-like' composition of interactors in the specification of complex interactive systems. A modal logic whose modalities are indexed by fragments of sets of actions is introduced to provide the common modelling language for both interactors and the coordination layer. The approach is illustratedwith a few examples.

Pre-Galois Connection on Coalgebras for Generic Component Refinement (Sun Meng)

The technique of Galois connections has been applied successfully in many areas of computer science. By employing coalgebras as models for software components, we claim that different forms of behavior model and types of state transitions for components are instances of a single form of coalgebra in a Kleisli category. Based on the Kleisli category, the results on forward/backward morphisms and refinement of components in Set are still satisfied in this more generic framework. We propose a notion of pre-Galois connection in the context of coalgebras for refinement of state-based software components which takes into consideration not only the refinement ordering but also the dynamics of the components, and we study its properties in the Kleisli category. This notion is a powerful tool for relating a component to its refinement and for relating a component to its abstraction. Thus it provides a basis for reasoning about state-based software designs and reverse engineering.

Discovering Coordination Patterns in Legacy Software (Nuno Rodrigues)

Legacy software systems often contain non trivial coordination logic to accomplish its operations or even to provide third-party services. As real world software solutions, such systems are often composed of different software layers which in turn, usually make use of different programming languages according to specific aspects of each layer. Even more, it is often the case that there is no access to the source code and the original system developers are not available anymore. Targeting this heterogeneous scenario, we present a method to lift coordination patterns from Intermediate Language and represent them in the orchestration language Orc, in which they become amenable to formal reasoning.

Flatten from/to Relational (Jacome Cunha)

Spreadsheets are considered one of the largest programming
languages in the world. Moreover, spreadsheet languages/systems lack recent and powerful programming features available in modern programming languages, namely powerful modular and type systems. As a result, programming in a spreadsheet environment is an error prone task.

In this talk we present a technique to overcome some of these problems. The flatten model of a spreadsheet if mapped into a relational database model.

A map from the fatten to the relational model is also presented.

Intentional automata (David Costa)

t.b.a.

Performance Analysis of Reo Circuits (Chretien Verhoef)

In this presentation a method is given to quantify the performance of complex coordination systems using the Reo coordination language. Quantifying the performance of complex coordination systems, for instance communication networks or web based services, is a very complex process. Hereby we want to take into account the stochastic behaviour of such complex coordination systems. One way to quantify the performance is by using Markov Chains (MC). Constructing the appropriate MC for these systems is a complicated task, and regularly leads to state space explosion of the MC. It is possible to model complex coordination systems using the Reo coordination language. Reo allows compositional construction of models for these systems using architecturally meaningful primitives. By adding quality of service properties to these functional primitives, we can compositionally construct the MC models for complex systems.

Translations from QIA to Markov Chains (Young-Joo Moon)

Reo language is a channel-based glue language for coordination models, and its operational semantics is given by Constraint Automata(CA). However, this semantics does not account for quantitative aspects derived from the environment, such as the requests arrival times, response times, and throughput rates. Markov Chains(MCs) are well-known stochastic models that can specify these quantities, however, it is difficult to specify a Reo system directly as a MC. We consider a translation from quantitative Reo language to Quantitative Intentional Automtata(QICA) considering the environment, and then from there to MCs. Therefore, we can model a system with its environment information in the quantitative Reo language, and obtain performance evaluation from the derived MC.