A partition analysis method to demonstrate program reliability
Debra J. Richardson · 1981
Program testing and program verification have long been considered unallied, competing approaches to demonstrating program reliability. Neither approach is infallible, yet if used in conjunction they can complement one another nicely. The partition analysis method takes this approach by integrating testing and verification in an attempt to counterbalance the weaknesses of each approach by the strengths of the other. By applying symbolic evaluation techniques to both an implementation and a specification of a problem, the method partitions the problem domain into subdomains so that all elements of each subdomain are treated uniformly by the specification and processed uniformly by the implementation. This partition provides the basis for the application of both verification and testing techniques. Several error sensitive testing techniques are employed to astutely select test data for each of the subdomains. Standard verification techniques are also utilized in the context of this partition to show that the implementation is consistent with the specification. Moreover, when integrated within partition analysis, the test data selection process and the verification process are used to enhance each other. This dissertation describes the partition analysis method and provides examples of its application. Some related work in program testing and program verification that have influenced the development of partition analysis are discussed. A specification language that is used in conjunction with the method is introduced. In addition, several areas for further research are considered.