Technical failure and human error are critical events in the occurrence of most accidents. When formally analysing an accident report, it would therefore be advantageous to use a formal notation well suited to modelling the behaviour of the human and technical entities active in the system. In this talk I will introduce SFOAL (Sorted First Order Action Logic), one such notation.
However, the recommendations in accident reports generally focus more on organisational arrangements and social factors in the system. Formal analysis of an accident report would therefore also benefit from the use of a notation well suited to modelling the legislative and organisational control structures which exist in the system. In this talk I will also introduce such a notation, a deontic extension to SFOAL. Deontic logics deal with the concepts of obligatory and permitted behaviour.
I will also discuss how these notations compare with some of the other notations being employed in accident analysis.