Research Grants in Verification for trustworthy critical real-time systems

HASLab is a research center based at Universidade do Minho (www.uminho.pt), one of the top state funded research universities in Portugal and in the top 3% of Scimago IBE ranking. We are part of the INESC TEC Associate Laboratory (http://www2.inescporto.pt/ip-en). HASLab research aims at improving scientific standards in software design through rigorous methods and mathematical techniques.

We are looking for PhD students and post-doctoral fellows willing to pursue work in the following broad topics:

· Development tools for the formal verification of critical interactive systems through model checking and theorem proving.

· The role of different verification tools – software model checkers, timed model checkers, theorem provers – in the verification of real time software applied to critical systems.

The applicants should possess a good honours MSc degree (for PhD applicants) / PhD degree (for post-doctoral applicants) in Computer Science or related disciplines. We particularly welcome candidates with experience in formal verification. Candidates should have a good command of English.

This call is open from June, 12th to June, 26th, 2013.

More information can be obtained though ERACareers:
– PhD student positions (references BIM-2013_BestCase_RL8.1_UMINHO and BIM-2013_BestCase_RL8.2_UMINHO): http://www.eracareers.pt/opportunities/index.aspx?task=global&jobId=36976
– Post-doctoral positions (references BPD-2013_BestCase_RL8.1_UMINHO and BPD-2013_BestCase_RL8.2_UMINHO): http://www.eracareers.pt/opportunities/index.aspx?task=global&jobId=36963

HASlab is located in the Braga Campus of Universidade do Minho. Braga is very close to the Peneda-Gerês Natural Park, and has good connections to Porto (and its vibrant cultural life) and the International Airport (30 min shuttle bus to Braga). It also has a very competitive cost of living in comparison to other European cities.

Any questions contact José Creissac Campos at jose.campos@di.uminho.pt

Advertisements

Research grants in CRDTs and Distributed Aggregation

We are opening several new positions  in HASLab, to be supported by (up to) two year research grants.

– One of the grants is for a Post Doc, to join the local team that is working on the evolution of CRDTs (Conflict-free Replicated Data Types). This is a very active research topic with growing impact in both industry and academia. We are looking for someone that can share our vision and work with us and our research associates. Possible research topics to be pursued by the successful candidate include the composition of CRDTs (with correctness proofs by construction), efficient update dissemination under different channel assumptions, and unification of state based and operation based models. Prospective candidates should check this announcement and apply for research line RL3.

– Another grant is aimed at candidates holding an MSc degree, to join our research line in Distributed Data Aggregation. The successful candidate is expected to research on distributed aggregation, e.g. Flow Updating and Extrema Propagation, and explore improvements to allow for faster and more reactive adaptation to changes in the network and monitored values. These research activities would be compatible with part-time enrollment in our PhD program, which the successful candidate will be encoraged to pursue. Prospective candidates should consult this announcement and apply for research line RL3.1.

HASLab has a very active research team in Large Scale Distributed Systems, working in both Systems and Theory. Our Laboratory is located in the Braga Campus of Universidade do Minho, one of the top state funded research universities in Portugal and in the top 3% of Scimago IBE ranking. We are part of the Associate Laboratory INESC TEC.  Braga is very close to the Gerês Natural Park, and has good connections to Porto (and its vibrant cultural life) and the International Airport (30 min shuttle bus to Braga). It also has a very competitive cost of living in comparison to other European cities.

This call is open from June, 12th to June, 26th, 2013.

Any questions, contact Carlos Baquero at cbm@di.uminho.pt

Scaling up Reconciliation in Eventual Consistency

Eventually consistent distributed stores have followed different strategies when it comes to deciding how to reconcile data that has diverged. A discussion last week led me to think a little bit on what can be done without knowing the semantics of the diverged data and what possibly cannot be done.

A first step is considering if a given system does detect divergence. Systems that use Last Writer Wins (LWWs), such as  Cassandra, do not detect divergence and simplify the process by deciding up front how divergence is reconciled, and that is LWWs. In these systems data is tagged with a timestamp that follows a total order  consistent with causality (ideally close to real time), so that related data is in the causally expected order, but concurrently evolved data will also appear to be ordered.

Another option is to track the causal evolution of data and accurately detect when concurrent writes have lead to divergent states (e.g. as possible in Riak). Now, these states can be presented to the application logic, or user,  that can try to resolve the conflict and create a new state that can causally overwrite the concurrent states.  This option is also followed in revision control systems where the programmer is responsible to resolve conflicts.

Marek Zawirski remembered me that LWW can be quite adequate if there is a single user updating the data. In this case, and if the system’s registered total order is not too far from real time, the user is actually making an external causal link across the data. In simpler terms, if I wrote “meet today” in a partition and I later wrote “better meet tomorrow” in another partition, I know that converging to “better meet tomorrow” is the correct option, although the two states would be presented as concurrent from a causal perspective. However, in general LWW leads to lost updates when multiple users do changes.

Now we come to the second option, track causally divergent states and present them for re-conciliation. If the rate of updates on a given data item is not very high, we can still expect the data to converge. Once two or more concurrent states occur, we only need to expect some user (say, a programer merging two versions of code) to read them and submit a merged state that subsumes the concurrent ones. However, if the merge is non deterministic, and other important properties are not met, we might run into a problem:

Each reconciliation decision is like an update and if we have multiple users trying to reconcile in parallel and even other users doing new updates one might never reduce concurrent state to a single copy, and the needed reconciliation will become more and more confusing so that in practical terms a converged state might not be reachable. This is a problem in what we can refer as syntactic reconciliation, and stems from only relying in causality, where we have no information on the internal structuring of the data and how it is reconciled. These approach only tracks how states relate in causal terms and which states safely subsume other preceding states.

So although tracking divergence and reducing concurrency by syntactic  reconciliation is in general better than LWW, there is probably a scalability limitation in this line of approach. When the data types permit so, a way around is to use information on the semantics of the data and automate reconciliation and make it behave more like an aggregation process, where intermediate reconciliations do not increase the complexity but instead help the progress towards a convergent state. To that end, reconciliation needs to be deterministic and exhibit certain properties: Associative, Commutative and Idempotent; form a join semi-lattice under a given partial order and LUB.

Such amenable data types, captured in Conflict-Free Replicated Data Types (CRDTs) designs and principled eventual consistency, still allow several options when considering viable system designs. One such option is to do merges at the server side and try to keep divergence at a minimum (see riak-dt). Another is to do it at the client side, something achievable with appropriate libraries (see toolbox, meangirls, knockbox and statebox) on top of any system that detects and presents concurrent states.

And certainly there is an interesting middle-ground to explore where semantic merging is done both at the edge (close to the clients) and at the core (in the DCs).

Folding the user into the analysis of system resilience

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).

Continue reading

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.

Continue reading

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.