Author Archives: José C. Campos

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.

Reasoning About Eventual Consistency with Replicated Data Types (Alexey Gotsman – IMDEA Software Institute)

HASLab Seminar

Abstract: Modern databases underlying large-scale Internet services
guarantee immediate availability and tolerate network partitions at the
expense of providing only weak forms of consistency, commonly dubbed
eventual consistency. Even though the folklore notion of eventual
consistency is very weak, in reality, the semantics and programming
interfaces of systems implementing it can be very subtle. In particular,
such systems can resolve conflicting updates using complex protocols,
called replicated data types (aka CRDTs), and can allow varying kinds of
anomalous behaviour.

So far the semantics provided by eventually consistent systems have been
poorly understood. I will present a novel framework for their formal
specification and discuss how recent nontrivial replicated data type
implementations fit into it. I will then illustrate the utility of the
framework by presenting techniques for proving the correctness of
replicated data type implementations.

This is joint work with Sebastian Burckhardt (Microsoft Research),
Hongseok Yang (University of Oxford) and Marek Zawirski (INRIA &
UPMC-LIP6). The associated paper appeared in POPL’14:
http://software.imdea.org/~gotsman/papers/distrmm-popl14.pdf

Link

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.

Link

Reusing models and properties in the analysis of similar interactive devices

Reusing models and properties in the analysis of similar interactive devices

Variations between user interface designs are often relatively subtle and do not always become evident through even relatively thorough user testing. Notwithstanding their subtlety, these differences may be important to the safety or usability of a device. To address this, we are using model checking techniques for checking systematically a set of template properties that are designed to explore important interface characteristics. We have applied the approach to two devices designed to support similar tasks in a clinical setting (two infusion pumps). The analysis of the two infusion pumps provides solid evidence of areas of concern where redesign would reduce complexity and increase the reliability of the two designs.

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

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.