Recently, a large body of research has been exploiting group communication based techniques to improve the dependability and performance of synchronously replicated database systems.

In this paper we propose the mutable consensus protocol, a pragmatic and theoretically appealing approach to enhance the performance of distributed consensus. First, an apparently inefficient protocol is developed using the simple stubborn channel abstraction for unreliable message passing. Then, performance is improved by introducing judiciously chosen finite delays in the implementation of channels. Although this does not compromise correctness, which rests on an asynchronous system model, it makes it likely that the transmission of some messages is avoided and thus the message exchange pattern at the network level changes noticeably. By choosing different delays in the underlying stubborn channels, the mutable consensus protocol can actually be made to resemble several different protocols. Besides presenting the mutable consensus protocol and four different mutations, we evaluate in detail the particularly interesting permutation gossip mutation, which allows the protocol to scale gracefully to a large number of processes by balancing the number of messages to be handled by each process with the number of communication steps required to decide. The evaluation is performed using a realistic simulation model which accurately reproduces resource consumption in real systems.

This paper presents a survey of Formal Methods courses in European higher education carried out by the FME Subgroup on Education over the last two years. The survey data sample is made of 117 courses spreading over 58 higher-education institutions across 13 European countries and involving (at least) 91 academic staff.
A total number of 365 websites have been browsed which are accessible from the electronic (HTML) version of this paper in the form of links to course websites, lecturers and topic entries in encyclopedias or virtual libraries.Three main projections of our sample are briefly analysed. Although far from being fully representative, these already provide some useful indicators about the impact of formal methods in European computing curricula.

This paper characterizes refinement of state-based software components modelled as pointed coalgebras for some Set endofunctors. The proposed characterization is parametric on a specification of the underlying behaviour model introduced as a strong monad. This provides a basis to reason about (and transform) state-based software designs.

The basic motivation of component based development is to replace conventional programming by the composition of reusable off-the-shelf units, externally coordinated through a network of connecting devices, to achieve a common goal. This paper introduces a new relational model for software connectors and discusses some preliminary work on its implementation in HASKELL. The proposed model adopts a coordination point of view in order to deal with components’ temporal and spatial decoupling and, therefore, to provide support for looser levels of inter-component dependency and effective external control.

Over the last decade, software architecture emerged as a critical design step in Software Engineering. This encompassed a shift from traditional programming towards the deployment and assembly of independent components. The specification of the overall system structure, on the one hand, and of the interactions patterns between its components, on the other, became a major concern for the working developer. Although a number of formalisms to express behaviour and supply the indispensable calculational power to reason about designs, are available, the task of deriving architectural designs on top of popular component platforms has remained largely informal. This paper introduces a systematic approach to derive, from behavioural specifications written in Ccs, the corresponding architectural skeletons in the Microsoft. Net framework in the form of executable C code. Such prototyping process is automated by means of a specific tool developed in Haskell.

With increasing use of computing systems while on the move and in constantly changing conditions, whether it is via mobile devices, wearable computers or embedded systems in the environment, time plays an increasingly important role in interaction. The way in which information is represented in an interface is fundamental to interaction with it, and how the information is used in the users tasks and activities. Dynamic representations where the user must perceive changes in the information displayed over time pose a further challenge to the designer. Very often this information is integrated with information from the environment in the performance of the user’s tasks. The diminutive size and limited display capabilities of many ubiquitous and mobile computing devices further motivate careful design of these displays. In this paper we look at how time can be taken into account when reasoning about representational issues from the early stages of design. We look at a model which can be used to reason about these issues in a structured fashion, and apply it to an example.