Recent Publications

Bonsangue M, Caltais G, Goriac E, Lucanu D, Rutten J, Silva A.  2011.  Automatic equivalence proofs for non-deterministic coalgebras (revised and extended). :1-38. Abstract18793d.pdf

A notion of generalized regular expressions for a large class of systems modeled as coalgebras, and an analogue of Kleene’s theorem and Kleene algebra, were recently proposed by a subset of the authors of this paper. Examples of the systems covered include infinite streams, deterministic automata, Mealy machines and labelled transition sytems. In this paper, we present a novel algorithm to decide whether two expressions are bisimilar or not. The procedure is implemented in the automatic theorem prover CIRC, by reducing coinduction to an entailment relation between an algebraic specification and an appropriate set of equations. We illustrate the generality of the tool with three examples: infinite streams of real numbers, Mealy machines and labelled transition systems.

Bonchi F, Bonsangue M, Boreale M, Rutten J, Silva A.  2011.  A coalgebraic perspective on linear weighted automata. :1-31. Abstract18069a.pdf

Weighted automata are a generalization of non-deterministic automata where each transition, in addition to an input letter, has also a quantity expressing the weight (e.g. cost or probability) of its execution. As for non-deterministic automata, their behaviours can be expressed in terms of either (weighted) bisimilarity or (weighted) language equivalence.

Coalgebras provide a categorical framework for the uniform study of state-based systems and their behaviours.
In this work, we show that coalgebras can suitably model weighted automata in two different ways: coalgebras on Set (the category of sets and functions) characterize weighted bisimilarity, while coalgebras on Vect (the category of vector spaces and linear maps) characterize weighted language equivalence.

Relying on the second characterization, we show three different procedures for computing weighted language equivalence. The first one consists in a generalization of the usual partition refinement algorithm for ordinary automata. The second one is the backward version of the first one. The third procedure relies on a syntactic representation of rational weighted languages.

Bonchi F, Hülsbusch M, König B, Silva A.  2011.  A coalgebraic perspective on minimization, determinization and behavioural metrics. :1-23. Abstract18079d_1.pdf

Coalgebra offers a unified theory of state based systems, including infinite streams, labelled transition systems and deterministic automata. In this paper, we use the coalgebraic view on systems to derive, in a uniform way, abstract procedures for checking behavioural equivalence in coalgebras, which perform (a combination of) minimization and determinization in the system. First, we show that for coalgebras on categories equipped with factorization structures, there exists an abstract procedure for equivalence checking. For instance, when considering epi-mono factorizations in the category of sets and functions, this procedure corresponds to the usual (coalgebraic) minimization algorithm and two states are behaviourally equivalent iff they are mapped to the same state in the minimized coalgebra. Second, motivated by several examples, we consider coalgebras on categories without suitable factorization structures: under certain conditions, it is possible to apply the above procedure after transforming coalgebras with reflections. This transformation can be thought of as some kind of determinization. Finally, we show that the result of the procedure also induces a pseudo-metric on the states, in such a way that the distance between each pair of states is minimized.

Silva A.  2011.  A specification language for Reo connectors. :1-17. Abstract18033d.pdf

Recent approaches to component-based software engineering employ coordinating connectors to compose components into software systems. Reo is a model of component coordination, wherein complex connectors are constructed by composing various types of primitive channels. Reo automata are a simple and intuitive formal model of context-dependent connectors, which provided a compositional semantics for Reo. In this paper, we study Reo automata from a coalgebraic perspective. This enables us to apply the recently developed coalgebraic theory of generalized regular expressions in order to derive a specification language, tailor-made for Reo automata, and sound and complete axiomatizations with respect to three distinct notions of equivalence: (coalgebraic) bisimilarity, the bisimulation notion studied in the original papers on Reo automata and trace equivalence. The obtained language is simple, but nonetheless expressive enough to specify all possible finite Reo automata. Moreover, it comes equipped with a Kleene-like theorem: we provide algorithms to translate expressions to Reo automata and, conversely, to compute an expression equivalent to a state in a Reo automaton.

Beckwith L, Cunha J, Fernandes JP, Saraiva JA.  2010.  End Users Productivity in Model-based Spreadsheets: An Empirical Study. Abstracttr_study.pdf

Spreadsheets are widely used by end users, and studies have shown that most end-user spreadsheets contain non-trivial errors. To improve end users productivity, recent research proposes the use of a model-driven engineering approach to spreadsheets. In this paper we conduct the first systematic empirical study to assess the effectiveness and efficiency of this approach. A set of spreadsheet end users worked with two different model-based spreadsheets, and we present and analyze the results achieved.

Cunha J, Visser J, Alves T, Saraiva JA.  2010.  Type-safe Evolution of Spreadsheets. Abstracttr_evolution.pdf

Spreadsheets are notoriously error-prone. To help avoid the introduction of errors when changing spreadsheets, models that capture the structure and interdependencies of spreadsheets at a conceptual level have been proposed. Thus, spreadsheet evolution can be made safe within the confines of a model. As in any other model/instance setting, evolution may not only require changes at the instance level but also at the model level. When model changes are required, the safety of instance evolution can not be guarded by the model alone. Coupled transformation of models and instances are supported by the 2LT platform and have been applied for transformation of algebraic datatypes, XML schemas, and relational database models. We have extended 2LT to spreadsheet evolution. We have designed an appropriate representation of spreadsheet models, including the fundamental notions of formulæ, references, and blocks of cells. For these models and their instances, we have designed coupled transformation rules that cover specific spreadsheet evolution steps, such as extraction of a block of cells into a separate sheet or insertion of columns in all occurrences of a repeated block of cells. Each model-level transformation rule is coupled with instance level migration rules from the source to the target model and vice versa. These coupled rules can be composed to create compound transformations at the model level that induce compound transformations at the instance level. With this approach, spreadsheet evolution can be made safe, even when model changes are involved.

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.