This Article 
 Bibliographic References 
 Add to: 
Is Proof More Cost-Effective Than Testing?
August 2000 (vol. 26 no. 8)
pp. 675-686

Abstract—This paper describes the use of formal development methods on an industrial safety-critical application. The Z notation was used for documenting the system specification and part of the design, and the SPARK1 subset of Ada was used for coding. However, perhaps the most distinctive nature of the project lies in the amount of proof that was carried out: proofs were carried out both at the Z level—approximately 150 proofs in 500 pages—and at the SPARK code level—approximately 9,000 verification conditions generated and discharged. The project was carried out under UK Interim Defence Standards 00-55 and 00-56, which require the use of formal methods on safety-critical applications. It is believed to be the first to be completed against the rigorous demands of the 1991 version of these standards. The paper includes comparisons of proof with the various types of testing employed, in terms of their efficiency at finding faults. The most striking result is that the Z proof appears to be substantially more efficient at finding faults than the most efficient testing phase. Given the importance of early fault detection, we believe this helps to show the significant benefit and practicality of large-scale proof on projects of this kind.

[1] T. Alspaugh, S. Faulk, K. Heninger Britton, R. Parker, D. Parnas, and J. Shore, “Software Requirements for the A7-E Aircraft,” Technical Report NRL/FR/5530-92-9194, Naval Research Laboratory, Washington, D.C., 1992.
[2] R. Barden, S. Stepney, and D. Cooper, Z in Practice. BCS Practitioner Series, Prentice-Hall, 1994.
[3] J. Barnes, High Integrity Ada: The SPARK Approach. Addison-Wesley, 1997.
[4] J.F. Bergeretti and B.A. Carr, “Information-Flow and Data-Flow Analysis of While-Programs,” ACM Trans. Programming Language and Systems, vol. 7, no. 1, Jan. 1985.
[5] C. Bolton, J. Davies, and J.C.P. Woodcock, “On the Refinement and Simulation of Data Types and Processes,” IFM99: Proc. 1st Int'l Conf. Integrated Formal Methods, K. Araki, A. Galloway, and K. Taguchi, eds. pp. 273–292, 1999.
[6] R.C. Chapman, A. Burns, and A.J. Wellings, “Combining Static Worst-Case Timing Analysis and Program Proof,” Real-Time Systems, vol. 11, no. 2, pp. 145–171, Sept. 1996.
[7] R.C. Chapman and R. Dewar, “Re-Engineering a Safety-Critical Application Using SPARK 95 and GNORT,” Reliable Software Technology: Proc. 1999 Ada Europe Conf., M.H. Harbour and J.A. de la Puente, eds., pp. 39–51, 1999.
[8] Software Productivity Consortium, “Consortium Requirements Engineering Guidebook,” Technical Report SPC-92060-CMC, Version 01. 00. 09, , Herndon, Va., 1993.
[9] D. Craigen, S.L. Gerhart, and T.J. Ralston, “An International Survey of Industrial Applications of Formal Methods,” Technical Report NIST GCR 93/626 vol. 1-2, Atomic Energy Control Board of Canada, U.S. Nat'l Inst. Standards and Technology, and U.S. Naval Research Laboratories, 1993.
[10] M. Croxford and J. M. Sutton, “Breaking Through the V and V Bottleneck” Ada in Europe 1995, M. Toussaint, ed., pp. 344–354, 1995.
[11] J. Fitzgerald, C.B. Jones, and P. Lucas, eds., , FME' 97: Proc. Industrial Application and Strengthened Foundations of Formal Methods, 1997.
[12] M.C. Gaudel and J.C.P. Woodcock, eds., , FME' 96: Industrial Benefit and Advances in Formal Methods, 1996.
[13] A. Hall, “Using Formal Methods to Develop an ATC Information System,” IEEE Software, vol. 13, no. 2, pp. 66–76, Mar. 1996.
[14] A. Hall, “What Does Industry Need From Formal Specification Techniques?” Proc. second IEEE Workshop on Industrial-Strength Formal Specification Techniques, Keynote Speech: 1998.
[15] M.G. Hinchey and J.P. Bowen, eds., Applications of Formal Methods. Englewood Cliffs, N. J.: Prentice-Hall, 1996.
[16] J. Jacky, The Way of Z: Practical Programming with Formal Methods. Cambridge Univ. Press, 1997.
[17] United Kingdom Ministry of Defence, , Hazard Analysis and Safety Classification of the Computer and Programmable Electronic System Elements of Defence Equipment. Technical Report, INTERIM DEF STAN 00-56. Apr. 1991.
[18] United Kingdom Ministry of Defence, The Procurement of Safety Critical Software in Defence Equipment. Technical Report, INTERIM DEF STAN 00-55 (Part 1: Requirements). Apr. 1991.
[19] United Kingdom Ministry of Defence, The Procurement of Safety Critical Software in Defence Equipment. Technical Report INTERIM DEF STAN 00-55 (Part 2: Guidance). Apr. 1991.
[20] K.A. Nyberg, ed., The Annotated Ada Reference Manual. Technical Report ANSI/MIL-STD-1815A, 1983.
[21] D.L. Parnas, G.J.K. Asmis, and J.D. Kendall, “Reviewable Development of Safety Critical Software,” Proc. Int'l Conf. Control and Instrumentation in Nuclear Installations, 1990.
[22] S.L. Pfleeger and L. Hatton, "Investigating the Influence of Formal Methods," Computer, Feb. 1997, pp. 33-43.
[23] Praxis Critical Systems, SPARK---The SPADE Ada Kernel, ed. 3.3, Aug. 1997.
[24] J.M. Spivey, The Z Notation: A Reference Manual, Prentice-Hall, Englewood Cliffs, N.J., 1992.
[25] S. Stepney, D. Cooper, and J.C.P. Woodcock, “More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement,” ZUM'98: the Z Formal Specification Notation, J.P. Bowen, A. Fett, and M.G. Hinchey, eds., pp. 284–307, 1998.
[26] I. Toyn and J.A. McDermid, “CADiZ: An Architecture for Z Tools and Its Implementation,” Software Practice and Experience, vol. 25, no. 3, pp. 305–330, Mar. 1995.
[27] J.C.P. Woodcock, “Mathematics as a Management Tool: Proof Rules for Promotion,” Software, for Large Software Systems, B.A. Kitchenham, ed., 1990.
[28] J.C.P. Woodcock and J. Davies, Using Z: Specification, Refinement and Proof. Prentice-Hall, 1996.

Index Terms:
Safety-critical software, formal specification, SPARK, specification proof, code proof, proof vs. testing, industrial case study.
Steve King, Jonathan Hammond, Rod Chapman, Andy Pryor, "Is Proof More Cost-Effective Than Testing?," IEEE Transactions on Software Engineering, vol. 26, no. 8, pp. 675-686, Aug. 2000, doi:10.1109/32.879807
Usage of this product signifies your acceptance of the Terms of Use.