Combining testing and correctness verification in software reliability assessment

The delivery of sophisticated control algorithms or system features via software is the driving force behind its increased use in safety-critical applications. The existence of software faults in these systems is not tolerable and a high degree of confidence that safety-critical systems meet their reliability requirements must be gained prior to their deployment. The transformational approach to software reliability assessment of process-control systems combines the strengths of formal verification and statistical sampling techniques in one unified framework. Partial program proofs are used to amplify the effect of test cases, i.e., they allow us to infer the behavior of the program for many inputs based on its behavior for one input. These transformations reduce the effective size of the input space, typically by eliminating one or more dimensions in the input space. In this paper, we report the application of the transformational reliability assessment approach to two control programs int he aerospace engineering domain: a simplified satellite pitch controller and an automatic airplane-landing program. Advantages of transformational approach include significant reduction in size (dimensionality) of input space domain, exact determination of minimal fault size, and reduced sensitivity of reliability estimate to variations in the operational profile.