Economics of software verification

ABSTRACT

How can we determine the added value of software verification techniques over the more readily available conventional testing techniques? Formal verification techniques introduce both added costs and potential benefits. Can we show objectively when the benefits will outweigh the cost?

REFERENCES

• 1: Cavano, J.P., and LaMonica, F.S., Quality assurance in future development environments. IEEE Software, Sept. 1987, pp. 26-34.
• 2: Dave E. Eckhardt , Alper K. Caglayan , John C. Knight , Larry D. Lee , David F. McAllister , Mladen A. Vouk , John J. P. Kelly, An Experimental Evaluation of Software Redundancy as a Strategy for Improving Reliability, IEEE Transactions on Software Engineering, v.17 n.7, p.692-702, July 1991 [doi>10.1109/32.83905]
• 3: Fenton, N., and Neil, M., New directions in software metrics. http://www.agena.co.uk/new_directions_metrics/start.h tm
• 4: Norman E. Fenton , Martin Neil, A Critique of Software Defect Prediction Models, IEEE Transactions on Software Engineering, v.25 n.5, p.675-689, September 1999 [doi>10.1109/32.815326]
• 5: Norman E. Fenton , Niclas Ohlsson, Quantitative Analysis of Faults and Failures in a Complex Software System, IEEE Transactions on Software Engineering, v.26 n.8, p.797-814, August 2000 [doi>10.1109/32.879815]
• 6: Herbert Hecht , Myron Hecht , Dolores R. Wallace, Toward More Effective Testing for High-Assurance Systems, Proceedings of the 2nd High-Assurance Systems Engineering Workshop, p.176-181, August 11-12, 1997
• 7: Gerard J. Holzmann, The Model Checker SPIN, IEEE Transactions on Software Engineering, v.23 n.5, p.279-295, May 1997 [doi>10.1109/32.588521]
• 8: Holzmann, G.J., and Smith, M.H., Automating software feature verification, Bell Labs Technical Journal, Vol. 5, No. 2, April-June 2000, pp. 72-87.
• 9: Jones, C., Applied software measurement. McGraw-Hill, 1991, p. 177.
• 10: Joyce, E., Is error-free software possible? Datamation, Feb. 18, 1989.
• 11: S. H. Kan , J. Parrish , D. Manlove, In-process metrics for software testing, IBM Systems Journal, v.40 n.1, p.220-241, January 2001
• 12: John D. Musa , Anthony Iannino , Kazuhira Okumoto, Software reliability: measurement, prediction, application (professional ed.), McGraw-Hill, Inc., New York, NY, 1989
• 13: C. H. West, Protocol validation in complex systems, Symposium proceedings on Communications architectures & protocols, p.303-312, September 25-27, 1989, Austin, Texas, United States
• 14: New York Times, Tuesday May 1, 2001, Section C, pp. 1-2.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Algorithms, Design, Measurement, Reliability, Verification

Keywords:
model checking, software verification, spin, testing