- the modelling and analysis of interactive devices with a particular emphasis on the user device dyad.
- the modelling and analysis of ubiquitous systems where there are many users, one might say crowds of users.
The common thread of both approaches is to articulate and prove properties of interactive systems to explore interactive behaviour as it influences the user, with a particular emphasis on interaction failure. The goal is to develop systematic techniques that can be packaged in such a way that they can be used effectively by developers.
The analysis of interactive devices
The main focus of this work has been the analysis of devices such as medical infusion pumps, in-car air conditioning systems and flight management systems. In order to analyse these devices a tool has been developed (IVY) [Campos & Harrison, 2008]. This tool supports a number of aspects of the modelling and analysis of interactive systems.
- IVY supports the editing of models. Models are described in a simple deontic logic of actions (MAL) that allows focus on the actions that the user engages in to control and adjust the device. The tool translates MAL models into SMV and invokes NuSMV [Cimatti and others, 2002] to check properties of the model.
- IVY provides property patterns and the means of instantiating properties associated with the patterns. The patterns are designed to probe aspects of the interactive behaviour of the device systematically in a process that is similar to the application of ?usability heuristics?. By using the IVY property editor it is possible to define a battery of properties to which the device can be subjected. These properties explore mode as well as the relationship between attributes of the device and what is visible about the device.
- IVY provides a trace visualizer that eases the exploration of counter-examples when properties fail. These counter-examples provide material for scenarios that potentially depict problematic situations in the use of the device.
This tool has been used to explore the use of information resources to restrict analysis to cognitively plausible paths [Doherty and others, 2008]. Information resource constraints express the information that it is assumed the user will use in order to help decide what to do next to achieve a goal.
Our recent work has concerned the development of models of medical infusion pumps developed by two manufacturers [Campos & Harrison, 2011]. These designs take interesting and in some cases subtly different design decisions. Two large models have been constructed by reusing a common module that captures the characteristics of the underlying pump. Both models have been analysed using a battery of properties that have been instantiated for the two models so that similar properties can be checked of the two devices.
The analysis of mobile and ubiquitous Systems
This research is concerned with the analysis of systems that combine public displays and hand-held personal devices. These systems provide relevant and tailored information to users in physical environments such as hospitals, shopping malls, airports or office environments. The success of such systems depends on effective testing and user evaluation. They must be natural to users, enabling an enhanced experience of the place in which the system is situated. The evaluation of these systems is often impractical within their designed target environments. We are exploring predictive models of the interactive behaviour of these environment designs that includes an understanding of the proposed context. Properties are required that relate to how the smart environment enhances activity and experiences of complex spaces.
We are interested in stochastic properties of systems involving multiple people, that is crowds of people interacting with the system [Massink and others, 2012; Harrison and Massink, 2010]. This work has included the exploration of emergency egress in an office building and out-patient behaviour in the context of a hospital department. The technique uses PEPA [Hillston, 1996] and a combination of fluid flow and simulation techniques.
We have also explored a mixed approach connecting formal (Petri-net based) models of the ubiquitous systems with virtual reality simulations of the target environment in order to support different levels of analysis, from empirical studies to formal verification [Silva and others 2012].