Abstract
This paper reports the lessons learnt about the benefits of using a formal verification tool like PVS to support field studies. The presentation is based on a field study in the healthcare domain which was designed to investigate the resilience of human behaviour in an oncology ward of a hospital. The automated reasoning tool PVS was used systematically to compare actual practice observed during the field study with normative behaviour described for example by user manuals for the devices involved. The approach helped (i) identify latent situations that could lead to hazard, and (ii) suggest situations likely to warrant further investigation as part of the field study. The main contribution of this paper is a set of detailed examples that illustrate how we used PVS during the field study, and how the tool led to insights. © 2012 Springer-Verlag.

Abstract
A systematic tool-based method is outlined that raises questions about the circumstances surrounding an incident: why it happened and what went wrong. The approach offers a practical and systematic way to apply a distributed cognition perspective to incident investigations, focusing on how available information resources (or the lack of them) may shape user action, rather than just on causal chains. This perspective supports a deeper understanding of the more systemic causes of incidents. The analysis is based on a higher order-logic model describing how information resources may have influenced the actions of those involved in the incident. The PVS theorem proving system is used to identify situations where available resources may afford unsafe user actions. The method is illustrated using a healthcare case study. © 2012 Springer-Verlag.

Abstract

Abstract
Ambulance control involves distributed group work using a mix of computer and communications technologies. The implementation of computer technologies has had mixed results in this area, evidenced by serious failures in the London Ambulance Service in 1992. Often failures are due to inadequate attention to integration of organizational and technical aspects of work. We report a field study of the organization of one aspect of the work of ambulance control, locating the scene of an emergency. The study was carried out in two ambulance control centres, one predominantly urban and highly computerized and the other largely rural and minimally computerized. Our analysis shows that the particulars of `locating the scene' are best seen in terms of the use of different technologies to link representations and represented. This research has implications for understanding task and context and the integration of technology and organization in design, particularly with respect to using similar computer-based technologies in both ambulance control centres.

Abstract

Abstract