Software Verification Using Partition Analysis.
Abstract
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 01, 1988
- Accession Number
- ADA190570
Entities
People
- Robert P. Graham Jr.
Organizations
- Air Force Institute of Technology