Proving properties of accidents

Accident reports are produced by regulatory and commercial authorities, such as the UK Air Accident Investigation Branch and the US National Transportation Safety Board, in response to most major accidents. These documents are intended to ensure that disasters do not recur. They, typically, contain accounts of the human and system failures that lead to major accidents. These descriptions are then used to identify the primary and secondary causes of the failure. Finally, recommendations are made so that the operators and regulators of safety-critical systems can avoid future accidents. Unfortunately, it is often difficult for readers to trace the way in which particular conclusions are drawn from the many hundreds of pages of evidence in these reports. Natural language arguments often contain implicit assumptions and ambiguous remarks that prevent readers from understanding the reasons why a particular conclusion was drawn from a particular accident. In contrast, this paper argues that mathematical proof techniques can be used to support the findings of accident investigations. These techniques enable analysts to formally demonstrate that a particular conclusion is justified given the evidence in a report. In doing so, it is possible to identify missing pieces of evidence, to identify ambiguities and to determine which items of evidence are critical to particular lines of argument. The later sections of this paper then introduce Conclusion, Analysis and Evidence diagrams. These can be used to communicate the results of a formal analysis. The intention is not to replace the natural argumentation structures that are currently used in accident reports. Rather, our aim is to increase our confidence that particular conclusions are well supported by the evidence that is presented within a report. Finally, we show how CAE diagrams may be used in conjunction with design rationale techniques that have been proposed to support the design of safety-critical applications. This helps to ensure that findings about previous failures are propagated into the subsequent development of future systems.