Principles for the Use of Formal Methods in Accident Investigations

- Summary Report EPSRC Grant GR/K55042 -

Chris Johnson

Department of Computing Science, University of Glasgow, Glasgow G12 8QQ.,

Accident reports are intended to ensure that the faults of previous systems are not propagated into future applications. They contain the analysis of many different experts: human factors specialists; control engineers; meteorologists etc. The insights of these investigators are typically separated into chapters that reflect the concerns and expertise of their authors. This separation leads to inconsistencies and omissions between different accounts. The innovative task in this proposal was, therefore, to develop constructive techniques that support the production of accident reports. My aims were:

1. To develop a set of coherent principles that can guide the application of formal methods during accident investigations.

2. To perform a critical evaluation of temporal logic as a means of improving the Piper Alpha and Kings Cross reports.

3. To conduct a critical evaluation of executable temporal logics as means of simulating the events leading to accidents.

These objectives were met. I used a range of temporal logics and simulation techniques to identify inconsistencies and omissions in over twenty accident reports. I extended this initial approach to identify differences between various accounts of the same incident. Viewpoint analysis and refinement techniques from Software Engineering help to identify contradictions between these different reports. This is useful if, for example, a company and a regulator disagree about the causes of a failure. In such circumstances, my techniques can establish whether a particular item of evidence, or a line of reasoning, is present in one report but omitted in another.

In order to demonstrate the feasibility of this approach I had to show that it would scale to complex accidents with multiple latent and immediate causes. I, therefore, used modular specification techniques derived from work on ObjectZ and validated the approach against five different case studies. This work yielded further benefits. I was able to build generic models for classes of accidents, such as railway collisions, that could then be instantiated and refined to include the details of a particular incident. All of these techniques were reported in journal and conference papers. Together they form a coherent set of principles that guide the application of formal notations to support accident investigation.

Not all of the results of this project were positive in terms of the specific techniques being proposed. The notations that I exploited were extremely useful in analysing the flow of events over time. However, they did not provide adequate means of documenting the more detailed psychological and managerial causes of those failures. A further limitation is that my use of logic abstracted away from many of the rhetorical techniques that form an essential part of most accident reports. For instance, an investigator may stress a line of argument by repeatedly presenting a particular item of evidence. Such details are lost during the formalisation process. My current research addresses these weaknesses. I have extended a number of design rationale and argumentation techniques to capture these rhetorical effects. I am also using cognitive models, including EPIC, to identify the more detailed psychological precursors of terms such as ‘high workload’ and ‘poor situation awareness’. This forms a bridge between my accident analysis techniques and the use of EPIC by NASA and DERA to support cockpit development.

This work has received several national and international awards. It was cited as one of two "key areas" in my department’s Queen’s Award for Research and Teaching. It was presented at invited talks to the 1998 US International Safety Systems Symposium and at a NASA Langley research symposium. Further exploitation is planned through ongoing collaboration with the UK Health and Safety Executive. As part of this grant, I held two workshops on Human Error and Systems Development with Nancy Leveson (MIT). These have now grown into an annual series of meetings that provide a common forum for human factors engineers, systems developers and regulators.

Project Publications:

[1] M.-O. Bes, Towards a Framework for the Use of Cognitive Models to Analyse Accident Reports. In Denise Pinnel and N. Leveson (eds.), 2nd Workshop on Human Error and Systems Development, Safeware Corporation, Seattle, USA, 1998.

[2] R. Botting and C.W. Johnson, A Formal and Structured Approach to the Use of Task Analysis in Accident Modelling, International Journal of Human Computer Systems, (49): 223-244, 1998.

[3] R. Botting and C.W. Johnson Using Reason's Model of Organizational Accidents in Formalizing Accident Reports, To appear in Cognition, Technology and Work Journal, 1999.

[4] R. Botting and C.W. Johnson A Generic Model of Time and Location in the Analysis of Railway Accidents, Submitted to Safety Science Journal, 1999.

[5] C.W. Johnson, Improving the Analysis of Human Error in Accident Reports, Submitted to special edition on Safety-Critical Interaction, ACM Trans. on Computer-Human Interaction, 1999.

[6] C.W. Johnson, Establishing the Correctness of Accident Reports, Submitted to Ergonomics Journal, 1999.

[7] C.W. Johnson, Representing the Impact of Time on Human Error and Systems Failure. Interacting with Computers (11)53-86, 1998.

[8] C.W. Johnson, The Role Of Error Tolerant Design In Minimising The Impact Of Risk, Journal of Safety Science, (22)1:195-214, 1996.

[9] C.W. Johnson, Reasoning About Human Error and System Failure for Accident Analysis. In S. Howard, J. Hammond and G. Lindgaard (eds.), Interact'97, Chapman and Hall, London, 331-338, 1997.

[10] C.W. Johnson, Proving Properties of Accidents. In C.M. Holloway and K.J. Hayhurst (eds.) 4th Langley Formal Methods Workshop, NASA Conference Publication 3356, 21-34, Langley Research Centre, Hampton, USA, 1997.

[11] C.W. Johnson, The Application Of Petri Nets To Reason About Human Factors Problems During Accident Analyses. In P. Palanque and R. Bastide (eds.) The Design, Specification And Verification Of Interactive Systems, Springer Verlag, Berlin, Germany, 93-112, 1995.

[12] C.W. Johnson, A First Step Towards the Integration of Accident Reports and Constructive Design Documents, Accepted for SAFECOMP'99, 1998.

[13] C.W. Johnson, Visualizing the Relationship between Human Error and Organizational Failure. Submitted to International Safety Systems Conference, 1999.

[14] C.W.Johnson, J.C. McCarthy and P.C. Wright, Using A Formal Language To Support Natural Language In Accident Reports, Ergonomics Journal, (38)6:1264-1283, 1995.

[15] C.W. Johnson and A.J. Telford. Using Formal Methods To Analyse Human Error And System Failure During Accident Investigations, Software Engineering Journal, (11)6:355-365, 1996.

[16] L. Love and C.W. Johnson , Using Extended Fault-Trees in Conjunction With Traditional Accident Reports. In S. Howard, J. Hammond and G. Lindgaard (eds.), Interact'97, Chapman and Hall, London, 102-103, 1997.

[17] L. Love and C.W. Johnson , Using Diagrams to Support the Analysis of System 'Failure' and Operator 'Error'. In H. Thimbleby, B. O'Conaill and P. Thomas (eds.) Proceedings of HCI'97, Springer Verlag, London, 245-262, 1997.

[18] L. Love and C.W. Johnson, Accident Fault Trees. In C.W. Johnson (ed.), 1st Workshop on Human Error and Systems Development, Glasgow Accident Analysis Group, University of Glasgow, GAAG-TR-97-2, 16-25, 1997.

[19] A.J. Telford and C.W. Johnson, Extending The Application Of Formal Methods To Analyse Human Error And System Failure During Accident Investigations, Department of Computer Science, University of Glasgow, Technical Report 1996-6, 1996.

[20] A.J. Telford and C.W. Johnson , Viewpoints for Accident Analysis, Submitted to Formal Aspects of Computing, 1999.