Towards a theory for integration of mathematical verification and empirical testing

From the viewpoint of a project manager who is responsible for the verification and validation (V&V) of a software system, mathematical verification techniques provide a potentially valuable addition to otherwise standard empirical testing. However, the value they add, both in terms of coverage and in fault detection, has been difficult to quantify. Potential cost savings from replacing testing with mathematical techniques cannot be realized until the tradeoffs can be quantified. This paper first describes a framework for a theory of software fault detection that is based on software reliability and formalized fault models. The novelty of this approach is that it takes into account the relative utility of the various tools for fault detection. Second, the paper describes a utility model for integrating mathematical and empirical techniques with respect to fault detection and coverage analysis for software. Third, the paper discusses how to determine the optimal combination of black-box testing, white-box (structural) testing and formal methods in V&V of a software system. Finally, a demonstration of how this utility model can be used in practice is offered using a case study from a NASA software system