Details of Grant 

EPSRC Reference:	GR/S67494/01
Title:	Formal verification and empirical validation for interactive systems: a study of human error
Principal Investigator:	Blandford, Professor A
Other Investigators:	Curzon, Professor P
Researcher Co-Investigators:
Project Partners:	Concordia University
Department:	UCL Interaction Centre
Organisation:	UCL
Scheme:	Standard Research (Pre-FEC)
Starts:	01 October 2004	Ends:	31 January 2008	Value (£):	221,460
EPSRC Research Topic Classifications:	Human-Computer Interactions
EPSRC Industrial Sector Classifications:	Information Technologies
Related Grants:	GR/S67500/01
Panel History:	Panel Date Panel Name Outcome 07 Aug 2003 People & Interactivity Panel (Tech) Aug 03 Deferred
Summary on Grant Application Form
The majority of high reliability systems depend on the behaviour of users, who may also be considered as components of the larger interactive system. We propose to apply machine-assisted proof to the design of interactive systems, incorporating a user description as a component of the formally modelled system. This will allow us to bring the detection and correction of classes of human errors within the scope of verification technology: failed proof provides insight into the underlying causes of erroneous interactive behaviour. Established results from cognitive science will be used as a starting point. However, many aspects of cognition have not yet been studied in a way that makes findings amenable to formal modelling, so we will also conduct empirical studies of selected aspects of cognition at the requisite level of detail. By this two-pronged approach, the project will deliver validated, formally verified models of interactive systems. In addition, we will investigate the use of formal models in a more lightweight way to provide a rigorous foundation for semi-formal analysis of human error in interactive systems, and the challenges of making such techniques available within design practice. A substantial case study will be used to validate the approach.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:	http://www.dcs.qmul.ac.uk/research/imc/hum/
Further Information:
Organisation Website: