On reviewing the current literature, a strong case emerges for grounding any work within an overall perspective that integrates the experience of safety engineering and the correctness of formal methods. Such a basis, it is argued, is necessary for an effective contribution to the delivery with assurance of life-critical software components.

Next, details of the framework are instantiated, based upon the provision of a common formal semantics to represent both the safety analysis and software models. A procedure, FTBuild, is provided for deriving formal requirements as part of the process of generating formalised fault trees. Work is then presented on establishing relations between formalised fault trees and models, extending results of other authors. Also given are some notions of (property) conformance with respect to the given requirements.

The formal approach itself is supported by the enhancement of the theory of conformance testing that has been developed for communication systems. The basis of this work is the detailed integration of already established theories: a testing system for process algebra (the Experimental System due to Hennessy and de Nicola) and a more general observation framework (developed by the LOTOSphere consortium). Notions of conformance and robustness are then examined in the context of refinement for the process algebra, (Basic) LOTOS, resulting in the adoption of the commonly accepted 'reduction' relation for which a proof is given that it is testable. Then a new algorithm is developed for a single (canonical) tester for reduction, which is unified in that it tests simultaneously for both conformance and robustness. It also allows, in certain cases, a straghtforward implementation as a Full LOTOS process with the ability to give some diagnostics in the case of failure. The text is supported by examples and some guidelines for use.

Finally, having established these foundations, the methodology is demonstrated on the Flexport protocol through two iterations of FTBuild which demonstrate how the activities of specification, safety analysis, validation and refinement are all brought together.

- Paul Trafford