Impact of Program Transformation on Software Reliability Assessment

The statistical sampling method is a theoretically sound approach for measuring the reliability of safety-critical software, such as control systems for nuclear power plants, aircrafts, space vehicles, etc. It has, however, some practical drawbacks, two of which are the large number of test cases needed to attain a reasonable confidence in the reliability estimate and the sensitivity of the reliability estimate to variations in the operational profile. One way of dealing with both of these issues is to combine statistical sampling with formal methods and attempt to verify complete program paths. This combination becomes especially effective if high usage paths are verified. However, the verification of complete paths is difficult to perform in practice and viable only when there is a high confidence in the correctness of the specification. In this paper we identify program transformations and partial proofs which have a measurable impact on the reliability assessment procedure. These m..