Software Verification Using Partition Analysis.
AIR FORCE INST OF TECH WRIGHT-PATTERSON AFB OH SCHOOL OF ENGINEERING
Pagination or Media Count:
Software verification is the process of determining whether a piece of software is reliable--whether it performs as it is supposed to. As traditionally performed, program verification can account for 40 percent or more of the development time and cost of a software product. In spite of this fact, released software is notorious for its unreliability. These two facts, the expense of our attempts at program verification and our limited success, have sustained a great deal of research interest directed at finding more effective methods. This thesis develops extensions to a promising new verification technique called Partition Analysis, developed by Debra J. Richardson 1981. Partition Analysis appears to be a powerful approach for identifying program faults, but in its current state can only be applied to single program modules that produce no side effects, including input or output. This thesis extends the applicability of Partition Analysis by permitting the use of procedure and function calls, thereby allowing complete programs to be analyzed. The result is a set of techniques for handling regular, nonrecursive procedure and function calls, separate methods for the analysis of recursive procedures and functions, and an approach to the larger problem of analyzing entire programs.
- Computer Programming and Software