Category Archives: Just Accepted

Prototyping and Analysing Ubiquitous Computing Environments using Multiple Layers

If ubiquitous computing (ubicomp) is to enhance physical environments then early and accurate assessment of alternative solutions will be necessary to avoid costly deployment of systems that fail to meet requirements. In the context of APEX, a project ending this month, we have developed a prototyping framework that combines a 3D Application Server with a behavior modeling tool. The contribution of this framework is that it allows exhaustive analysis of the behaviour models that drive the prototype while at the same time enabling immersive exploration of a virtual environment simulating the proposed system. The development of prototypes is supported through three layers: a simulation layer (using OpenSimulator); a modelling layer (using CPN Tools) and a physical layer (using external devices and real users). The APEX framework allows movement between these layers to analyze different features, from user experience to user behaviour. The multi layer approach makes it possible to express user behavior in the modelling layer, provides a way to reduce the number of real users needed by adding simulated avatars, and supports user testing of hybrids of virtual and real components as well as exhaustive analysis. This paper demonstrates the approach by means of an example, placing particular emphasis on the simulation of virtual environments, low cost prototyping and the formal analysis capabilities.

Formal Verification of kLIBC with the WP Frama-C plug-in

Accepted at Nasa Formal Methods 2014.

by Nuno Carvalho, Cristiano da Silva Sousa, Jorge Sousa Pinto, and Aaron Tomb

Abstract: This paper presents our results in the formal verification of klibc, a minimalistic C library, using the Frama-C WP tool. We report how we were able to completely verify a significant number of functions from <string.h> and <stdio.h>. We discuss difficulties encountered and describe in detail a problem in the implementation of common <string.h> functions, for which we suggest alternative implementations.

Our work shows that it is presently already viable to verify low-level C code, with heavy usage of pointers. Although the properties proved tend to be shallower as the code becomes of a lower-level nature, it is our view that this is an important direction towards real-world software verification, which cannot be attained by focusing on deep properties of cleaner code, written specifically to be verified.


Analysing interactive devices based on information resource constraints

Analysing interactive devices based on information resource constraints

Analysis of the usability of an interactive system requires both an understanding of how the system is to be used and a means of assessing the system against that understanding. Such analytic assessments are particularly important in safety-critical systems as latent vulnerabilities may exist which have negative consequences only in certain circumstances. Many existing approaches to assessment use tasks or scenarios to provide explicit representation of their understanding of use. These normative user behaviours have the advantage that they clarify assumptions about how the system will be used but have the disadvantage that they may exclude many plausible deviations from these norms. Assessments of how a design fails to support these user behaviours can be a matter of judgement based on individual experience rather than evidence. We present a systematic formal method for analysing interactive systems that is based on constraints rather than prescribed behaviour. These constraints capture precise assumptions about what information resources are used to perform action. These resources may either reside in the system itself or be external to the system. The approach is applied to two different medical device designs, comparing two infusion pumps currently in common use in hospitals. Comparison of the two devices is based on these resource assumptions to assess consistency of interaction within the design of each device.

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.

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.

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.