Proving Properties of Accidents

Chris Johnson

Abstract

Accident reports are published by commercial and regulatory organisations, such as the UK Air Accident Investigation Branch and the US National Transportation Safety Board, after all major accidents. They are intended to prevent the recurrence of similar failures in other systems. Unfortunately, traditional reporting techniques frequently fail to satisfy this objective. A range of common causes can be identified in accidents ranging from Kegworth, through to the Herald of Free Enterprise and Hillsborough.

Many of the problems with traditional reporting techniques stem from the difficulty of presenting several different lines of investigation in natural language documents. The different persepctives offered by human factors, software engineering, metallurgical, meteorological accounts make it different to form a coherent view of the events leading to major failure s. This, in turn, leads to significant ommissions and inconsistencies between the different strands of analysis within many reports.

In this talk, I will use a range of formal methods to identify errors in acciden t reports. A first order temporal logic will be used to construct a time-line for the events leading to a `failure'. This model will then be used to formally pr ove that the conclusions in an accident report are actually consistent with the events described in the report. If such a proof cannot be constructed then eit her there is an error in the formalisation OR there is an error in the accident repo rt itself.

If time allows, I will also show how formal refinement techniques can be used to identify political/organisational bias within accident reports.



Coping with Context (Draft abstract...)

I had originally planned to talk about the following but I want more time to develop the ideas and gather evidence... This talk will address two problems that frustrate the development of accident reports for complex, interactive systems.

What is the context of an accident?

In order to write a report, we must first decide which events were critical in the course of an accident. We must identify the initiating events. We must identify the events that were necessary for the 'propagation' of these initial failures. We must identify the events that helped to shape any response to an accident. Different reports often show wide variations in the events that they describe. These biases reflect the commercial or political pressures that help to shape an account. As such, they prevent readers from constructing an 'impartial' analysis of major accidents.

What do we mean by causality?

The omission of information from accident reports forces authors to adopt a number of complex reasoning techniques in order to convince readers that their analysis is valid. For example, removing information about a system failure forces analysts to 'tailor' their accounts of how the accident progressed. Some events may be reported in minute detail while others are glossed over. This leaves the reader to infer complex causal relationships from minimal evidence.

Focus of the Talk

I will begin by presenting a series of examples drawn from reports produced by the US Coast Guard, the Air Accident Investigation Branch and US Presidential Boards of Inquiry. These examples will then be used to illustrate a technique for formally identifying bias in documents. This technique not only identifies missing information between two accounts, it also provides means of reasoning about the inferences that are lost when critical information is ommitted.

Although the focus will be on accident reports, many of the same arguments could be made about requirements documents in both software engineering and interface design. Partial information and individual biases have a profound impact upon the inferences that a designer can make about a potential systems. By hiding information about design requirements, it is possible to bias key development decisions.

Finally, I will explain why Steve Draper and Phil Gray had an accident on the way to the GIST meeting...

Everyone is invited back to Chris and Fionnuala's for drinks after the talk. (You'll probably need it...?)