Abstract
A transition system can be presented either as a binary relation or as a coalgebra for the powerset functor, each representation being obtained from the other by transposition. More generally, a coalgebra for a functor F generalises transition systems in the sense that a shape for transitions is determined by F, typically encoding a signature of methods and observers. This paper explores such a duality to frame in purely relational terms coalgebraic refinement, showing that relational (data) refinement of transition relations, in its two variants, downward and upward (functional) simulations, is equivalent to coalgebraic refinement based on backward and forward morphisms, respectively. Going deeper, it is also shown that downward simulation provides a complete relational rule to prove coalgebraic refinement. With such a single rule the paper defines a pre-ordered calculus for refinement of coalgebras, with bisimilarity as the induced equivalence. The calculus is monotonic with respect to the main relational operators and arbitrary relator F, therefore providing a framework for structural reasoning about refinement.

Abstract
Tool interoperability as a mean to achieve integration is among the main goals of the international Grand Challenge initiative. In the context of the Verifiable file system mini-challenge put forward by Rajeev Joshi and Gerard Holzmann, this paper focuses on the integration of different formal methods and tools in modelling and verifying an abstract file system inspired by the Intel Flash File System Core. We combine high-level manual specification and proofs with current state of the art mechanical verification tools into a tool-chain which involves Alloy, VDM++ and HOL. The use of (pointfree) relation modelling provides the glue which binds these tools together. © 2009 Springer-Verlag Berlin Heidelberg.

Abstract
The pointfree transform offers to the predicate calculus what the La-place transform offers to the differential/integral calculus: the possibility of changing the underlying mathematical space so as to enable agile algebraic calculation. This paper addresses the foundations of the transform and its application to a calculational approach to extended static checking (ESC) in the context of abstract modeling. In particular, a calculus is given whose rules help in breaking the complexity of the proof obligations involved in static checking arguments. The close connection between such calculus and that of weakest pre-conditions makes it possible to use the latter in ESC proof obligation discharge, where pointfree notation is again used, this time to calculate with invariant properties to be maintained. A connection with the "everything is a relation" lemma of Alloy is established, showing how close to each other the pointfree and Alloy notations are. The main advantage of this connection is that of complementing pen-and-paper pointfree calculations with model checking support wherever validating sizable abstract models.

Abstract

Abstract
This paper introduces a generic technique to obtain a shared-storage database cluster from an off-the-shelf database management system, without needing to heavily refactor server software to deal with distributed locking, buffer invalidation, and recovery from partial cluster failure. Instead, the core of the proposal is the combination of a replication protocol and a surprisingly simple modification to the common copy-on-write logical volume management technique: One of the servers is allowed to skip copy-on-write and directly update the original backing store. This makes it possible to use any shared-nothing database server software in a shared or partially shared storage configuration, thus allowing large cluster configurations with a small number of copies of data. Copyright 2009 ACM.

Abstract
Gossip, or epidemic, protocols have emerged as a highly scalable and resilient approach to implement several application level services such as reliable multicast, data aggregation, publish-subscribe, among others. All these protocols organize nodes in an unstructured random overlay network. In many cases, it is interesting to bias the random overlay in order to optimize some efficiency criteria, for instance, to reduce the stretch of the overlay routing. In this paper we propose X-BOT, a new protocol that allows to bias the topology of an unstructured gossip overlay network. X-BOT is completely decentralized and, unlike previous approaches, preserves several key properties of the original (non-biased) overlay (most notably, the node degree and consequently, the overlay connectivity). Experimental results show that X-BOT can generate more efficient overlays than previous approaches.