Many safety-critical applications rely upon complex interaction between computer systems and their users. When accidents occur, regulatory bodies are called upon to investigate the causes of user ‘error’ and system ‘failure’. Reports are drawn up so that the designers and operators of future systems will not repeat previous ‘mistakes’. These documents present the work of specialists who are drawn from many different technical disciplines: human factors; forensic investigation; engineering reconstruction; computer simulation; etc. The findings of these different experts are often separated into different sections. This creates a number of problems. Important evidence can be hidden within numerous appendices. The interaction between systems and users can be obscured by tortuous cross referencing schemes. There are occasional temporal ambiguities and inconsistencies between the different analyses. This paper presents ways in which formal methods can be exploited to address these problems. Mathematical notations provide means of representing and reasoning about the circumstances that lead to accidents in human machine systems. Executable logics can also be used to simulate event sequences. These simulations might be shown to other analysts. They can be used to encourage agreement on the course of events prior to more detailed investigations.

Keywords: safety-critical systems, temporal logics, formal methods, simulation.

Introduction

Accident reports are intended to ensure that the faults of previous systems are not propagated into future applications. For example, the Presidential investigation into the Three Mile Island accident led the United States' Nuclear Regulatory Commission (NRC) to adopt a policy of minimal intervention (Pew, Miller & Feehrer, 1981). Whenever possible operators should not be required to intervene in order to preserve the safety of their system.