University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Pragmatic application of formal methods to safety critical systems.

Pratt, Norman Derek. (1996) Pragmatic application of formal methods to safety critical systems. Doctoral thesis, University of Surrey (United Kingdom)..

Available under License Creative Commons Attribution Non-commercial Share Alike.

Download (39MB) | Preview


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.

Item Type: Thesis (Doctoral)
Divisions : Theses
Authors :
Pratt, Norman Derek.
Date : 1996
Contributors :
Depositing User : EPrints Services
Date Deposited : 09 Nov 2017 12:13
Last Modified : 15 Mar 2018 23:09

Actions (login required)

View Item View Item


Downloads per month over past year

Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800