The systematic analysis of interactive devices to explore potential problems that might arise through their use provides an important element in the design of new systems or the analysis of existing systems. The use of behavioral models, focusing on the system and supported by automated reasoning, to analyze human-computer interaction has been the subject of previous research [1, 2, 3, 4] but how best to fold the user into the analysis of system resilience remains an open problem. We are currently working on a technique that tackles this issue by narrowing the model checking analysis of interactive systems to cognitively plausible behaviours (those behaviours that are likely to be carried out by users because the device or the user’s training or some other contextual factor leads to it).
Newly funded research: Test case generation and execution for misuses
Model-based testing methods automate the generation of test cases from a model of the system under test. However, in the particular case of interactive systems, the fact that oracles typically describe the normative operation of a system presents a problem. Being normative, the oracles do not capture the common mistakes that users might make, or alternatives to the expected normative usage. However, in the case of interactive systems, the quality of the systems is also linked to how the system reacts to user error.
In the context of the PBGT (Pattern-Based GUI Testing) project, recently funded by FCT, we will focus on user errors (indeed, more generally, on unexpected user behaviours), and how they can be integrated into the model-based testing approach being developed in the project. To that end, we will explore the generation of test case mutations. Typical test cases express the expected “correct” user behaviour defined for each GUI pattern. The mutated test cases will express typical user errors, in order to test the GUI against erroneous user behaviour.
To achieve its stated goal, the task will develop an algorithm to carry out changes (mutations) to the test cases. These mutated test cases will capture the effect of the different types of errors on the interface. This will be done by building on previous work by members of the project as described in [1].
[1] A. Barbosa, A. Paiva and J.C. Campos. Test case generation from mutated task models. In ACM Symposium on Engineering Interactive Computing Systems (EICS 2011), pages 175-184. ACM.
Model-checking graph properties using Alloy
While developing an algorithm for fast distributed computation of a graph diameter and radius, some of my colleagues had a conjecture about graph topology that, if true, would enable an aggressive optimization of the algorithm.
In order to understand the conjecture we must first recall some (more or less) standard graph theory definitions:
- The distance between two nodes is the length of the shortest path between them;
- The eccentricity of a node is the greatest distance between that node and all others;
- The diameter of a graph is the maximum eccentricity found in the graph;
- A node is peripheral if its eccentricity is equal to the diameter;
- The antipode of a node is the set of nodes at distance equal to its eccentricity.
Given a non-directed connected graph the initial conjecture was:
For every node, all nodes in its antipode are peripheral.
They quickly found a counter-example to this conjecture and relaxed it to the following:
For every node, some node in its antipode is peripheral.
For a long time they were not able to prove or refute this conjecture. At some point I was involved in the discussion and decided to model-check it using Alloy before attempting any proof.
Posted in Alloy, Distributed Systems
Conflict-free Replicated Data Types
A follow up to the paper in this post, was just accepted to SSS 2011. The focus of the new paper is around the following contributions:
- A solution to the CAP problem, Strong Eventual Consistency (SEC).
- Formal definitions of Strong Eventual Consistency (SEC) and of CRDTs.
- Two sufficient conditions for SEC.
- A strong equivalence between the two conditions.
- We show that SEC is incomparable to sequential consistency.
- Description of basic CRDTs, including integer vectors and counters.
- More advanced CRDTs, including sets and graphs.
Regarding CAP, what we explore is how must consistency can we deliver, without compromising Availability and Partition Tolerance. This is captured by the notion of Strong Eventual Consistency (SEC), that is formalized in the paper.
Any subset of replicas of a SEC object eventually converge, independently of the fate of the remaining replicas. They only need to deliver messages. Therefore a SEC object tolerates up to n − 1 simultaneous crashes. A SEC object thus fills an interesting space given by the CAP theorem: it is (eventually) consistent without sacrificing availability and partition-tolerance. Remarkably, SEC does not require to solve consensus.
We also introduce a SEC compliant Directed-Graph CRDT that allows concurrent Vertice and Edge addition and removal, with a semantics compatible with concurrent web crawling.
The associated TR is available here.
Posted in Distributed Systems, Just Accepted
Version Vectors are not Vector Clocks
Most people still confuse Version Vectors and Vector Clocks. Well, I did confuse them for several years. In fact they look the same and the update rules are almost the same.
Both of these mechanisms are practical ways of capturing causality in distributed systems. Causality (in distributed systems) is an abstract concept, can was formalized in 1978 by Leslie Lamport in one of the most cited articles in computer science. In 1983 Version Vectors are developed to track the causal relations among data items that can be concurrently updated. Some years later, around 1988, Vector Clocks are developed to track the causality between events in a distributed computation. In both cases a vector of integers, one per source of concurrency, is used. There is, however, a fundamental difference.
First, in order to simplify a little bit, lets consider that we have a fixed number of processes and a fixed number of replicas.
- Vector Clocks need to establish a partial order among a, potentially ever growing, set of events occurring in the processes. The set of events that are generated in the distributed computation. Naturally since the set can grow unbounded, the tracking mechanism also needs to grow unbounded. Vectors of integers are fine since, at least in theory we don’t run out of integers. In 1991, Charron-Bost showed in this article that Vector Clocks are the smaller mechanism that can track causality among distributed events.
- Version Vectors need to establish a partial order (more precisely a pre-order) among the replicas in the distributed system. Notice that although the state in these replicas changes as consequence of ever growing sets of update events, here we want to relate the replica states and not the update events. Using vectors of integers is over-expressive in this setting. In 2004, we noticed this and constructed Bounded Version Vectors, where integers are substituted by a limited set of symbols, depending on the number of replicas. Naturally, Charron-Bost result does not apply to Version Vectors.
Lets consider a simple example, thats shows that vectors of integers are over-expressive . One has two recently synchronized replicas A and B with identical state and vectors A[2,3] and B[2,3]. Now, replica A suffers an update and its new vector is A[3,3]. We now see that A is more updated than B, since [3,3] > [2,3] (here each integer in the left is greater or equal than its counterpart in the same position). Now replica A suffers 7 more updates, A[10,3]. Still we have [10,3] > [2,3], and this increase in the integer does not convey more information to the task of tracking the causal order among the two replicas. The number of individual updates is typically not important, specially in systems where you can change either a lot or a little in a single update. What is important is how they change the causal order relation among the replicas.
In the example, at this point, we can compare A[10,3] and B[2,3] and notice that they are easy to synchronize since A has the most updated state and it can be simply copied into B. However, if B issues an update and we now have a system with A[10,3] and B[2,4]. Now the replicas are divergent and a synchronization will typically have to look at the state (often with user assistance) to figure the correct synchronized state that can be tagged with [10,4].
Posted in Distributed Systems
Convergent and Commutative Replicated Data Types
We just published in the Bulletin of the European Association for Theoretical Computer Science, EATCS, a contribution to the management of eventual consistency. The current activity on Cloud systems design, NoSQL approaches, and the implications of the CAP Theorem are bringing increasing attention to eventual consistency.
In this paper we establish the conditions for eventual consistent datatypes (with no rollback allowed) and present two equivalent implementation flavors: State Based, with a defined merge operation and constraints that ensure that mutating operations are compatible with merge; Operation Based, building on top of a causal delivery middleware and ensuring that concurrent operations commute.
An extended version of this article is also available via INRIA and includes a larger portfolio of datatypes.
Posted in Just Accepted
Translating Alloy Specifications to UML Class Diagrams Enriched with OCL
Just accepted to SEFM’11
Joint work with Ana Garis and Daniel Riesco.
Abstract: Model-Driven Engineering (MDE) is a Software Engineering approach based on model transformations at different abstraction levels. It prescribes the development of software by successively transforming
models from abstract (specifications) to more concrete ones (code).
Alloy is an increasingly popular lightweight formal specification
language that supports automatic verification. Unfortunately, its
widespread industrial adoption is hampered by the lack of an
ecosystem of MDE tools, namely code generators. This paper presents
a model transformation between Alloy and UML Class Diagrams enriched
with OCL. The proposed transformation enables current UML-based
tools to also be applied to Alloy specifications, thus unleashing
its potential for MDE.
Posted in Just Accepted