Pragmatic application of formal methods to safety critical systems.

Formal Methods started primarily as a software development method, but now embrace a wide spectrum of purposes and techniques. This report considers one possible application of Formal Methods to Safety Critical Systems, namely its use in validation of a mechanism for a safety critical system. The technique involves construction of a Formal Model covering the mechanism, the real world aspects of interest, and the safety requirement. The technique supports exploring the behaviour of mechanisms in a mathematical way, and in particular establishing whether the behaviour complies with a safety property. The technique enables the analysis of mechanisms with complex behaviour, such as software based mechanisms, to be treated with a confidence not achievable with informal techniques such as Fault Tree Analysis. Proof has the power to show the absence of errors, and this is quite unlike the basis of other safety analysis techniques. It is this potential of proof which enables Formal Modelling to deal succinctly with the enormous numbers of cases typical of software mechanisms. The critical issue with Formal Modelling is Validity, ensuring the conclusions generated are valid in the real world. The approach adopted is based on the standard mathematical modelling method employed by Applied Mathematics. A variety of typical Formal Methods techniques are then integrated into this method to customise it. This integration is shown to be readily achieved, and results in a powerful Formal Modelling method. Certain pragmatic difficulties are identified. Chief amongst these is the considerable skill and experience needed to master the mathematical basis of the method. Overall, the conclusion is that Formal Modelling is a new analysis technique that is both complementary and supplementary to existing Safety Analysis techniques