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 SPARK subset of Ada was used for coding. However, perhaps the most distinctive nature of the project lies in the amount of proof which 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 9000 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 a comparison 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 was substantially more efficient at finding faults than the most efficient testing phase. Given the importance of early fault detection, this helps to demonstrate the significant benefit and practicality of large-scale proof on projects of this kind.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
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.
R. Barden, S. Stepney, and D. Cooper. Z in practice. BCS Practitioner Series. Prentice-Hall, 1994.
J. Barnes. High integrity Ada: The SPARK approach. Addison-Wesley, 1997.
J.-F. Bergeretti and B.A. Carré. Information-flow and data-flow analysis of while-programs. ACM Trans. Prog. Lang. Sys., 7(1), January 1985.
C. Bolton, J. Davies, and J.C.P. Woodcock. On the refinement and simulation of data types and processes. In K. Araki, A. Galloway, and K. Taguchi, editors, IFM99: Proceedings of the 1st International Conference on Integrated Formal Methods, pages 273–292. Springer-Verlag, 1999.
R.C. Chapman, A. Burns, and A.J. Wellings. Combining static worst-case timing analysis and program proof. Real-Time Systems Journal, 11(2):145–171, September 1996.
R.C. Chapman and R. Dewar. Re-engineering a safety-critical application using SPARK 95 and GNORT. In M.H. Harbour and J.A. de la Puente, editors, Reliable Software Technology: Proceedings of the 1999 Ada Europe Conference, Santander, Spain, number 1622 in Lecture Notes in Computer Science, pages 39–51. Springer-Verlag, 1999.
Consortium Requirements Engineering Guidebook. Technical Report SPC-92060-CMC Version 01.00.09, Software Productivity Consortium, Herndon, VA, USA, 1993.
D. Craigen, S. L. Gerhart, and T. J. Ralston. An international survey of industrial applications of formal methods. Technical Report NIST GCR 93/626-V1 & 2, Atomic Energy Control Board of Canada, US National Institute of Standards and Technology, and US Naval Research Laboratories, 1993.
M. Croxford and J.M. Sutton. Breaking through the V and V bottleneck. In M. Toussaint, editor, Ada in Europe 1995, volume 1031 of Lecture Notes in Computer Science, pages 344–354. Springer-Verlag, 1995.
J. Fitzgerald, C. B. Jones, and P. Lucas, editors. FME’97: Industrial Application and Strengthened Foundations of Formal Methods, volume 1313 of Lecture Notes in Computer Science. Formal Methods Europe, Springer-Verlag, 1997.
M.-C. Gaudel and J. C. P. Woodcock, editors. FME’96: Industrial Benefit and Advances in Formal Methods, volume 1051 of ecture Notes in Computer Science. Formal Methods Europe, Springer-Verlag, 1996.
A. Hall. Using formal methods to develop an ATC information system. IEEE Software, 13(2):66–76, March 1996.
A. Hall. Keynote speech: What does industry need from formal specification Techniques? In 2nd IEEE Workshop on Industrial-Strength Formal Specification Techniques, 1998.
M.G. Hinchey and Bowen, J.P., editors. Applications of Formal Methods. Prentice-Hall International series in computer science / C.A.R. Hoare, series editor. Prentice-Hall International, Englewood Cliffs, N.J.; London, 1996.
J. Jacky. The way of Z: Practical programming with formal methods. Cambridge University Press, Cambridge, UK, 1997.
MOD. Hazard analysis and safety classi cation of the computer and programmable electronic system elements of defence equipment. UK Ministry of Defence, April 1991. INTERIM DEF STAN 00-56.
MOD. The procurement of safety critical software in defence equipment. UKMinistry of Defence, April 1991. INTERIM DEF STAN 00-55 (Part 1: Requirements).
MOD. The procurement of safety critical software in defence equipment. UK Ministry of Defence, April 1991. INTERIM DEF STAN 00-55 (Part 2: Guidance).
K.A. Nyberg, editor. The annotated Ada Reference Manual. ANSI, 1983. ANSI/MIL-STD-1815A-1983.
D.L. Parnas, G.J.K. Asmis, and J.D. Kendall. Reviewable development of safety critical software. In Proceedings of the International Conference on Control and Instrumentation in Nuclear Installations, 1990.
S.L. Pfleeger and Hatton L. Investigating the influence of formal methods. IEEE Computer, 30(2):33–43, February 1997.
SPARK — The SPADE Ada Kernel. Praxis Critical Systems, August 1997. Edition 3.3.
J.M. Spivey. The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edition, 1992.
S. Stepney, D. Cooper, and J.C.P. Woodcock. More powerful Z data refinement: Pushing the state of the art in industrial refinement. In J.P. Bowen, A. Fett, and M.G. Hinchey, editors, ZUM’98: the Z formal specification notation, volume 1493 of Lecture Notes in Computer Science, pages 284–307. Springer-Verlag, 1998.
I. Toyn and J.A. McDermid. CADiZ: An architecture for Z tools and it implementation. Software — Practice and Experience, 25(3):305–330, March 1995.
J.C.P. Woodcock. Mathematics as a management tool: Proof rules for promotion. In B.A. Kitchenham, editor, Software Engineering for Large Software Systems. Elsevier, 1990.
J.C.P. Woodcock and J. Davies. Using Z: specification, refinement and proof. Prentice-Hall International series in computer science / C.A.R. Hoare, series editor. Prentice Hall, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
King, S., Hammond, J., Chapman, R., Pryor, A. (1999). The value of verification: positive experience of Industrial proof. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1709. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48118-4_31
Download citation
DOI: https://doi.org/10.1007/3-540-48118-4_31
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66588-5
Online ISBN: 978-3-540-48118-8
eBook Packages: Springer Book Archive