Human intervention has played a critical role in the causes of many major accidents. At Three Mile Island, the operators isolated a reactor from its heat sink. The pilots of the Boeing 737 at Kegworth managed to shut down their one functioning engine. Staff continued to allow trains to deposit passengers in Kings' Cross after the fire had started. In retrospect, it seems impossible to predict all of the ways that human intervention might threaten safety. It is, therefore, important that we learn as much as possible from those accidents that do occur. This task is complicated because conventional accident reports contain many hundreds of pages of prose. They present findings drawn from many different disciplines: metallurgy; systems engineering; human factors; meterology. These findings are, typically, separated into a number of distinct chapters. Each section focuses upon a different aspect of the accident. This makes it difficult for designers to recognize the ways in which operator intervention and system failure combine during major failures. The following pages use formal methods to address these concerns. It is argued that mathematical specification techniques can represent human factors and system failures. Unfortunately, formal methods have not previously been used to analyse the factors that motivate operator intervention. This paper, therefore, argues that epistemic extensions of mathematical notations must be recruited in order to support the formal analysis of major accidents. (C) 1997 Academic Press Limited.
