Extended Abstract:

This talk will describe recent attempts to improve accident reports. Existing techniques provide weighty volumes that are often full of contradictions, inconsistencies and ambiguities. These problems arise partly from the reporting process itself and partly from the more general difficulties of producing complex technical documents in multi-disciplinary groups.

Over the last three years, I have been using a range of formal specification techniques to identify the omissions and inconsistencies in existing accident reports, including the Kings Cross, Piper Alpha and Kegworth documents. I have used textual notations, such as temporal logic, as well as graphical techniques, including Petri Nets. The intention has been to provide an unambiguous representation of the events that lead to major accidents. These formal representations provide a common point of reference that avoid the ambiguity and omissions in reports. Unfortunately, this approach is almost useless as it stands.

Formal specifications provide most of the people involved in the reporting process with an extremely poor impresion of what caused an accident. It is difficult to validate the event structures that are built to represent the events leading to failures. I have, therefore, been working on `literate specification' techniques to address this problem. This approach integrates formal and semi-formal representations, such as design ratinale, so that readers can not only answer questions about what factors led to an accident but also why . The semi-formal representations are intended to be accessible to non-formalists including human factors experts and ergonomists. We will discuss issues of tool support and of conformance between informal and formal notations. I will also discuss the findings of a recent usability evaluation of this approach with some real software engineers from a rail service supplier and an international banking group.

Although our focus will be upon accident reports, a secondary theme will be the claim that our `literate specification' techniques provide a general tool for the application of formal methods. Our approach, arguably, provides the best available means of addressing the usability problems that prevent the wide-spread application of mathematical specifications.