Professor Michael Harrison

My research is carried out under two headings:

Modelling and systematic analysis of interactive systems

Current research on this topic includes exploring mechanisms for proving properties of specifications interactive behaviour using model checkers [Campos & Harrison, 2001, 2003]. This work focuses on the IVY tool developed by Jose Campos at University of Minho which supports the instantiation of standard property templates to a particular model. These templates can be applied systematically to analyse interactive devices [Campos & Harrison, 2008, 2009, 2011] and [Harrison, Campos & Masci, 2013} and the use of information resources to restrict analysis to cognitively plausible paths [Doherty, Campos & Harrison, 2008, Dittmar & Harrison, 2010, Campos, Doherty and Harrison]. This research is progressing as part of my half time research fellowship at QMUL in the context of medical instruments. More recent research has considered the complementary role of model checking and theorem proving in the analysis of interactive devices, see for example [Masci et al. 2013].


Mobile and Ubiquitous Systems

Systems combining public displays and hand-held personal devices will become a ubiquitous information environment for visitors (passengers, patients etc.) within complex spaces such as airports, hospitals, museums, retail and leisure complexes. These systems provide relevant and tailored information and services. 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. Such systems have a number of features that differentiate their evaluation from more "traditional" interactive systems. These differences arise because of:

  • the significant contribution of the environment and of experience in the acceptability of the system
  • the fact that location and context are used by the system to infer user action: activity is implicit or incidental rather than goal orientated

The evaluation of these systems is often impractical within their designed target environments. It becomes even more important therefore to provide predictive models of the interactive behaviour of the design and to simulate the proposed context for purposes of prototyping. Properties will be analysed relating to how the embedding of the ambient and mobile system within its environment enhances activity and experiences of complex spaces.

I am interested in:

  • developing generic models of the interactive behaviour of classes of ambient and mobile systems
  • developing a software architecture consistent with the model to enable practical exploration of usability of the environment through the use of prototypes.
  • checking (within the model) and exploring (with virtual prototypes
    using appropriately developed metaphors) usability properties of particular system examples drawing conclusions about the relative value of techniques

We are interested in recent work on generic models of publish subscribe architectures. This work factors the development of models into two parts:

  1. reusable model components that capture run-time event management and dispatch
  2. components that are specific to the publish subscribe application being modelled.

We are also interested in the problem of developing software in parallel. This may provide groundwork for an agile framework in which prototypes and models may be developed consistent with each other. The present concern (which differs from the protocol properties of these generic models) is with the problem of

  1. analysing the interaction that is being designed and how it supports users in their activities in the space (validating assumptions about the interaction) [Harrison and others, 2007; Harrison and others, 2008];
  2. analysing whether the system that is being designed supports the designed interaction (understand, evaluate and justify changes made to the software) [Silva and others, 2009].
  3. Stochastic properties of systems involving multiple people, that is crowds of people interacting with the system [Massink and others, 2008;2010; 2011; 2012; Harrison and others, 2009; 2010].

(1) is concerned with modelling and investigating the interaction between devices and users - exploring whether given a set of (dynamically) available resources (in some place, and at some point in time), users will be able to achieve certain goals. This analysis does not require detailed models of the software so that different design alternatives can be explored. (2) is concerned with modelling and investigating the "system" - having defined a set of necessary resources is it possible to explore whether the "system" provides those resources adequately (in the right place, at the right time, and according to the users' goals). 

I teach half a module of software safety as part of the Newcastle advanced MSc.