Recent Publications

Preguiça N, Moreno CB, Almeida PS, Fonte V, Gonçalves R.  2010.  Dotted Version Vectors: Logical Clocks for Optimistic Replication. CoRR. 1011.5808 Abstractdvv-arxiv.pdf

In cloud computing environments, a large number of users access data stored in highly available storage systems. To provide good performance to geographically disperse users and allow operation even in the presence of failures or network partitions, these systems often rely on optimistic replication solutions that guarantee only eventual consistency. In this scenario, it is important to be able to accurately and efficiently identify updates executed concurrently. In this paper, first we review, and expose problems with current approaches to causality tracking in optimistic replication: these either lose information about causality or do not scale, as they require replicas to maintain information that grows linearly with the number of clients or updates.Then, we propose a novel solution that fully captures causality while being very concise in that it maintains information that grows linearly only with the number of servers that register updates for a given data element, bounded by the degree of replication.

Silva A, Bonchi F, Bonsangue M, Rutten J.  2010.  Generalizing the powerset construction, coalgebraically. 8:1-12. Abstract16981d.pdf

Coalgebra is an abstract framework for the uniform study of different kinds of dynamical systems. An endofunctor $F$ determines both the type of systems ($F$-coalgebras) and a notion of behavioral equivalence ($\sim_F$) amongst them. Many types of transition systems and their equivalences can be captured by a functor $F$. For example, for deterministic automata the derived equivalence is language equivalence, while for non-deterministic automata it is ordinary bisimilarity. The powerset construction is a standard method for converting a nondeterministic automaton into an equivalent deterministic one as far as language is concerned. In this paper, we lift the powerset construction on automata to the more general framework of coalgebras with structured state spaces. Examples of applications include partial Mealy machines, (structured) Moore automata, and Rabin probabilistic automata.

Moon Y-J, Silva A, Krause C, Arbab F.  2010.  A Compositional Semantics for Stochastic Reo Connectors. :1-20. Abstract16529d_1.pdf

In this paper we present a compositional semantics for the channel-based coordination language Reo which enables the analysis of quality of service (QoS) properties of service compositions. For this purpose, we annotate Reo channels with stochastic delay rates and explicitly model data-arrival rates at the boundary of a connector, to capture its interaction with the services that comprise its environment. We propose Stochastic Reo automata as an extension of Reo automata, in order to compositionally derive a QoS-aware semantics for Reo. We further present a translation of Stochastic Reo automata to Continuous-Time Markov Chains (CTMCs). This translation enables us to use third- party CTMC verification tools to do an end-to-end performance analysis of service compositions.

Silva A, Bonsangue M, Rutten J.  2010.  Non-deterministic Kleene Coalgebras. :1-39. Abstract14942d.pdf

In this paper, we present a systematic way of deriving (1) languages of (generalized) regular expressions, and (2) sound and complete axiomatizations thereof, for a wide variety of systems. This generalizes both the results of Kleene (on regular languages and deterministic finite automata) and Milner (on regular behaviours and finite labelled transition systems), and includes many other systems such as Mealy and Moore machines.

Gonzalez-Sanchez A, Abreu R, Gross H-G, van Gemund A.  2010.  Improving the Software Fault Localization Process through Testability Information. :20. Abstracttud-serg-2010-011.pdf

When failures occur during software testing, automated software fault localization helps to diagnose their root causes and identify the defective components of a program to support debugging. Diagnosis is carried out by selecting test cases in such way that their pass or fail information will narrow down the set of fault candidates, and, eventually, pinpoint the root cause. An essential ingredient of effective and efficient fault localization is the knowledge about the intermittency of occurring failures, i.e., the rate at which defective components of a program will exhibit failures. In current fault localization processes, intermittency is either ignored completely, or merely estimated a posteriori as part of the diagnosis. In this paper, we study the reduction in testing and diagnosis effort when intermittency is known a priori. We deduce intermittency from testability, following the propagation-infection-execution (PIE) approach. Experiments with synthetic and real programs suggest significant improvement in the combined testing and diagnos is process. When compared to the next best technique, testability-based intermittency information reduces the average number of tests required to reach the same diagnosis quality by 55%, and provides an effort reduction for fault localization of 30% for the same testing effort.

Shoker A, Bahsoun JP.  2009.  BFT for Three Decades, Yet Not Enough!. :1-6. AbstractPaper

Distributed systems are established to maintain safety and liveness while attending good performance. Nowadays, Byzantine Failures are considered the most critical threat for system’s safety. Various BFT protocols were found through the history; however, none has been adopted yet. The reason perhaps originates from the fact that Byzantine Fault Tolerance issue is hard by nature; add to this the complications underlying BFT protocols implementation. This paper represents a general overview on Byzantine Fault Tolerance, its evolution, and difficulties disturbing its realization. First, we introduce the subject by defining replication, its importance and some problems; then we describe in brief the basic BFT protocols reporting some comparisons. Then we expose some problems that BFT protocols implementations are facing and we give a solution proposed by Guerraoui et al.; finally, we summarize our paper and conclude.

Bonsangue M, Clarke D, Silva A.  2009.  A model of context-dependent component connectors. :1-39. Abstract14628d.pdf

Recent approaches to component-based software engineering employ coordinat- ing connectors to compose components into software systems. For maximum flexibility and reuse, such connectors can themselves be composed, resulting in an expressive calculus of connectors whose semantics encompasses complex combinations of synchronisation, mutual exclusion, non-deterministic choice and state-dependent behaviour. A more expressive notion of connector includes also context-dependent behaviour, namely, whenever the choices a connector can take change non-monotonically as the context, given by the pending activity on its ports, changes. Context dependency can express notions of priority and inhibition. Capturing context-dependent behaviour in formal models is non-trivial, as it is unclear how to propagate context information through composition. In this paper we present an intuitive automata-based formal model of context- dependent connectors, and argue that it is superior to previous attempts at such a model for the coordination language Reo.

George C, Garis A.  2008.  SAL translator user guide. 1:113-149. Abstractsal-userguide.pdf

This is a user guide for the “rsltc” RAISE tool. This provides type checking; pretty-printing; generation of confidence conditions; showing module dependencies; translation to Standard ML, to C++, and to PVS; and translation to RSL from UML class diagrams. The user guide provides full instructions on the use and installation of this tool on Unix, Linux, and Windows platforms.

Silva A, Rutten J.  2007.  A coinductive calculus of binary trees. Abstract11938d.pdf

We study the set TA of infinite binary trees with nodes labelled in a semiring A from a coalgebraic perspective. We present coinductive definition and proof principles based on the fact that TA carries a final coalgebra structure. By viewing trees as formal power series, we develop a calculus where definitions are presented as behavioural differential equations. We present a general format for these equations that guarantees the existence and uniqueness of solutions. Although technically not very difficult, the resulting framework has surprisingly nice applications, which is illustrated by various concrete examples.

Bonsangue M, Rutten J, Silva A.  2007.  Regular expressions for polynomial coalgebras. Abstract11926d.pdf

For polynomial set functors G, we introduce a language of expressions for describing elements of final G-coalgebra. We show that every state of a finite G-coalgebra corresponds to an expression in the language, in the sense that they both have the same semantics. Conversely, we give a compositional synthesis algorithm which transforms every expression into a finite G-coalgebra. The language of expressions is equipped with an equational system that is sound, complete and expressive with respect to G-bisimulation.

Bonsangue M, Rutten J, Silva A.  2007.  Coalgebraic logic and synthesis of Mealy machines. :1-15. Abstract11925d.pdf

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.

Silva A, Rutten J.  2007.  Behavioural differential equations and coinduction for binary trees. Abstract11939d.pdf

We study the set TA of infinite binary trees with nodes labelled in a semiring A from a coalgebraic perspective. We present coinductive definition and proof principles based on the fact that TA carries a final coalgebra structure. By viewing trees as formal power series, we develop a calculus where definitions are presented as behavioural differential equations. We present a general format for these equations that guarantees the existence and uniqueness of solutions. Although technically not very difficult, the resulting framework has surprisingly nice applications, which is illustrated by various concrete examples.

Abreu R, Zoeteweij P, Van Gemund AJC.  2006.  Program Spectra Analysis in Embedded Software: A Case Study. :12. Abstract0607116.pdf

Because of constraints imposed by the market, embedded software in consumer electronics is almost inevitably shipped with faults and the goal is just to reduce the inherent unreliability to an acceptable level before a product has to be released. Automatic fault diagnosis is a valuable tool to capture software faults without extra effort spent on testing. Apart from a debugging aid at design and integration time, fault diagnosis can help analyzing problems during operation, which allows for more accurate system recovery. In this paper we discuss perspectives and limitations for applying a particular fault diagnosis technique, namely the analysis of program spectra, in the area of embedded software in consumer electronics devices. We illustrate these by our first experience with a test case from industry.

Moreno CB, Lopes N.  2004.  B Trees on P2P: Providing content indexing over DHT overlays. :1-5. Abstractbtp2p-techrep_2.pdf

The ability to search by content has been at the core of P2P data sharing systems and is a fundamental tool in the modern Web. However, currently deployed P2P search technology still suffers from either excessive centralization, abuse of network resources or low accuracy.
Efcient overlay structuring systems, like distributed hash tables (DHTs), provide adequate solutions to content location as long as unique identiers are used. They cannot, however, directly support search without negative impacts on the load balance of data distribution among peer nodes. We will show that DHTs can be used as a base for efcient content indexing by building a BTree structure that coordinates the use of homogeneous size blocks,
compatible with the DHT load balance assumptions. The remaining of the paper is dedicated
to a discussion of some of the issues, problems and possible solutions, that need to considered when building complex data structures on top of a peer-to-peer DHT layer.