Queen Mary, University of London logo HUM project logo UCL logo

HUM project

Work packages

Studies of human error

Human Error Modelling (HUM) Project

Formal verification and empirical validation of interactive systems:
a study of human error

HUM is a joint project between the Department of Computer Science at Queen Mary, University of London and University College London Interaction Centre. It has been awarded funding by EPSRC on research agreements GR/S67494/01 and GR/S67500/01, and runs from September 2004 until January 2008. The work builds on that of the earlier PUMA project.

stop pressPlease consider making a submission to the 2nd International Workshop on Formal Methods for Interactive Systems (FMIS-2007). This workshop is being co-organised by the HUM Project.

The project aims to make theoretical advances in HCI by taking a cross-disciplinary approach. Recognising the need for rigorous systems development processes that explicitly take account of users' needs and capabilities, it brings together work in formal methods, cognitive science and design to explore synergies and creative tensions between the different approaches. The overall aim of the project is to determine to what extent and how results from cognitive science can be integrated with formal verification technology, and what it might take to make formally grounded, empirically tested insights readily accessible to design practitioners. The focus is on understanding and representing various classes of user errors (as opposed to other aspects of user experience such as speed of interaction and user satisfaction). The specific objectives of the research are to:

  • develop a formal, generic user model, based on results from cognitive science, that supports reasoning about interactive behaviour and implements key features of user cognition that often result in 'human error';
  • perform empirical validation of key features of the formal user model, conducting experiments that check the model's predictions against actual user behaviour when using interactive systems;
  • develop and test an appropriate methodology for applying the formal user model with complementary device specifications to reason about interactive behaviour, including investigating how to make the methodology scale to large designs based on successful approaches from other verification domains;
  • perform a detailed study of the factors that contribute to selected classes of human error when working with interactive systems that are covered by the formal user model;
  • investigate how formal user models can be used in a lightweight way for semi-formal analysis, providing maximum leverage from time-consuming formal work outside the design cycle itself; and
  • study design practice, particularly focusing on the design of high reliability socio-technical systems, investigating how such an approach can usefully be integrated with design practice.


This page last modified 11 September, 2007 by George Papatzanis


IMC logo
Logo of EPSRC
go to UCLIC home page