Advertisement

The industrial take-up of formal methods in safety-critical and other areas: A perspective

  • Jonathan Bowen
  • Victoria Stavridou
Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 670)

Abstract

Formal methods may be at the crossroads of acceptance by a wider industrial community. In order for the techniques to become widely used, the gap between theorists and practitioners must be bridged effectively. In particular, safety-critical systems offer an application area where formal methods may be engaged usefully to the benefit of all. This paper discusses some of the issues concerned with the general acceptance of formal methods and concludes with a summary of the current position and how the formal methods community could proceed to improve matters in the future.

Keywords

Software Engineering Software Engineer Formal Method Formal Notation Computer Control System 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Safety related computer controlled systems market study. A review for the Department of Trade and Industry by Coopers & Lybrand in association with SRD-AEA Technology and Benchmark Research (HMSO, London, 1992)Google Scholar
  2. 2.
    The Procurement of Safety Critical Software in Defence Equipment (Part 1: Requirements, Part 2: Guidance). Interim Defence Standard 00-55, Issue 1, Ministry of Defence, Directorate of Standardization, Kentigern House, 65 Brown Street, Glasgow G2 8EX, UK (5 April 1991)Google Scholar
  3. 3.
    Barden, R., Stepney, S., Cooper, D.: The use of Z. In Nicholls, J.E. (ed.): Z User Workshop, York 1991 (Springer-Verlag, Workshops in Computing, 1992) pp. 99–124Google Scholar
  4. 4.
    Barroca, L., McDermid, J.: Formal methods: use and relevance for the development of safety critical systems. The Computer Journal 35 6 (December 1992)CrossRefGoogle Scholar
  5. 5.
    Bjørner, D.: Trusted computing systems: the ProCoS experience. Proc. 14th International Conference on Software Engineering (ICSE), Melbourne, Australia (11–14 May 1992)Google Scholar
  6. 6.
    Blyth, D., Bolddyreff, C., Ruggles, C., Tetteh-Lartey, N.: The case for formal methods in standards. IEEE Software (September 1990) 65–67Google Scholar
  7. 7.
    Bowen, J.P.: Formal specification in Z as a design and documentation tool. Second IEE/BCS Conference, Software Engineering 88, Conference Publication No. 290 (July 1988) pp. 164–168Google Scholar
  8. 8.
    Bowen, J.P.: Towards verified systems (Elsevier, Real-time Safety-critical Systems Series, 1993) In preparationGoogle Scholar
  9. 9.
    Bowen, J.P., Stavridou, V.: Safety-critical systems, formal methods and standards. Technical Report PRG-TR-5-92, Programming Research Group, Oxford University Computing Laboratory, UK (1992) Revised version to appear in the Software Engineering Journal Google Scholar
  10. 10.
    Bowen, J.P., Stavridou, V.: Formal methods and software safety. In [17] (1992) pp. 93–98Google Scholar
  11. 11.
    Buxton, J.N., Malcolm, R.: Software technology transfer. Software Engineering Journal 6 1 (January 1991) 17–23Google Scholar
  12. 12.
    Coleman, D.: The technology transfer of formal methods: what's going wrong? Proc. 12th ICSE Workshop on Industrial Use of Formal Methods, Nice, France (March 1990)Google Scholar
  13. 13.
    Craigen, D., Gerhart, S., Ralston, T.J.: An international survey of industrial applications of formal methods. Atomic Energy Control Board of Canada, U.S. National Institute of Standards and Technology, and U.S. Naval Research Laboratories (1993) To appearGoogle Scholar
  14. 14.
    Craigen, D., Gerhart, S., Ralston, T.J.: Formal methods reality check: industrial usage. In Formal Methods Europe Symposium (FME'93) (Springer-Verlag, LNCS, 1993) In this volumeGoogle Scholar
  15. 15.
    Deransart, P.: Prolog standardisation: the usefulness of a formal specification, on comp.lang.prolog, comp.specification and comp.software-eng electronic usenet newsgroups (October 1992)Google Scholar
  16. 16.
    Dyer, M.: The Cleanroom approach to quality software development (Wiley Series in Software Engineering Practice, 1992)Google Scholar
  17. 17.
    Frey, H.H. (ed.): Safety of computer control systems 1992 (SAFECOMP'92). Computer Systems in Safety-critical Applications, Proc. IFAC Symposium, Zürich, Switzerland, 28–30 October 1992 (Pergamon Press, 1992)Google Scholar
  18. 18.
    Good, D.I., Young, W.D.: Mathematical methods for digital system development. In Prehn, S., Toetenel, W.J. (eds.): VDM '91, Formal Software Development Methods, Volume 2: Tutorials (Springer-Verlag, LNCS 552, 1991) pp. 406–430Google Scholar
  19. 19.
    Guiho, G., Hennebert, C.: SACEM software validation. Proc. 12th International Conference on Software Engineering (ICSE) (IEEE Computer Society Press, March 1990) pp. 186–191Google Scholar
  20. 20.
    Hall, J.A.: Seven myths of formal methods. IEEE Software (September 1990) 11–19Google Scholar
  21. 21.
    Harrison, M.D.: Engineering human error tolerant software. In Nicholls, J.E. (ed.): Z User Workshop, York 1991 (Springer-Verlag, Workshops in Computing, 1992) pp. 191–204Google Scholar
  22. 22.
    Hill, J.V.: Software development methods in practice. Proc. COMPASS '91: 6th Annual Conference on Computer Assurance (1991)Google Scholar
  23. 23.
    Hoare, C.A.R.: Let's make models. In Baeten, J.C.M., Klop, J.W. (eds.): Proc. CONCUR '90 (Springer-Verlag, LNCS 458, 1990)Google Scholar
  24. 24.
    Houston, I., King, S: CICS project report: experiences and results from the use of Z in IBM. In Prehn, S., Toetenel, W.J. (eds.): VDM '91, Formal Software Development Methods (Springer-Verlag, LNCS 551, 1991) pp. 588–603Google Scholar
  25. 25.
    IEEE standard glossary of software engineering terminology. In IEEE Software Engineering Standards Collection (Elsevier Applied Science, 1991)Google Scholar
  26. 26.
    Josephs, M.B., Redmund-Pyle, D.: Entity-relationship models expressed in Z: a synthesis of structured and formal methods, Technical Report PRG-TR-20-91, Programming Research Group, Oxford University Computing Laboratory, UK (July 1991)Google Scholar
  27. 27.
    Learmount, D.: Airline safety review: human factors. Flight International 142 4238 (22–28 July 1992) 30–33Google Scholar
  28. 28.
    Liskov, B., Guttag, J.: Abstraction and Specification in Program Development (MIT Press, 1986)Google Scholar
  29. 29.
    MacKenzie, D.: Computers, formal proof, and the law courts. Notices of the American Mathematical Society 39 9 (November 1992) 1066–1069Google Scholar
  30. 30.
    May, D., Barrett, G., Shepherd, D.: Designing chips that work. In Hoare, C.A.R., Gordon, M.J.C. (eds.): Mechanized reasoning and hardware design (Prentice Hall International Series in Computer Science, 1992) pp. 3–19Google Scholar
  31. 31.
    Moore, J.S. et al., Special issue on system verification. Journal of Automated Reasoning 5 4 (1989) 409–530Google Scholar
  32. 32.
    Neesham, C.: Safe conduct. Computing (12 November 1992) 18–20Google Scholar
  33. 33.
    Nicholls, J.E.: A survey of Z courses in the UK. In Nicholls, J.E. (ed.), Z User Workshop, Oxford 1990 (Springer-Verlag, Workshops in Computing, 1991) pp. 343–350Google Scholar
  34. 34.
    Normington, G.: Cleanroom and Z. In Bowen, J.P., Nicholls, J.E. (eds.), Z User Workshop, London 1992 (Springer-Verlag, Workshops in Computing, 1993) To appearGoogle Scholar
  35. 35.
    Pyle, I.: Software engineers and the IEE. Software Engineering Journal 1 2 (March 1986) 66–68Google Scholar
  36. 36.
    Potocki de Montalk, J.P.: Computer software in civil aircraft. Microprocessors and Microsystems. In Cullyer, W.J. (ed.): Special issue on safety critical systems (1993) To appearGoogle Scholar
  37. 37.
    Ravn, A.P., Stavridou, V.: Project organisation. In Bjørner, D., Langmaack, H., Hoare, C.A.R.: Provably Correct Systems, chapter 9, part 1, ESPRIT BRA 3104 ProCoS Technical Report (1992) Available from Department of Computer Science, DTH, Lyngby, DenmarkGoogle Scholar
  38. 38.
    Redmill, F., Anderson, T.: Safety-critical systems — current issues, techniques and standards (Chapman and Hall, 1993)Google Scholar
  39. 39.
    Stein, R.M.: Safety by formal design. BYTE (August 1992) p. 157Google Scholar
  40. 40.
    Stepney, S., Barden, R., Cooper, D. (eds.): Object orientation in Z (Springer-Verlag, Workshops in Computing, 1992)Google Scholar
  41. 41.
    Thomas, M.C.: The industrial use of formal methods. Microprocessors and Microsystems. In Cullyer, W.J. (ed.): Special issue on safety critical systems (1993) To appearGoogle Scholar
  42. 42.
    Tierney, M.: The evolution of Def Stan 00-55 and 00-56: an intensification of the “formal methods debate” in the UK. Proc. Workshop on Policy Issues in Systems and Software Development, Science Policy Research Unit, Brighton, UK (July 1991)Google Scholar
  43. 43.
    Wallace, D.R., Kuhn, D.R., Ippolito, L.M.: An analysis of selected software safety standards. IEEE AES Magazine (August 1992) 3–14Google Scholar
  44. 44.
    Wing, J.M., Zaremski, A.M.: Unintrusive ways to integrate formal specifications in practice. In Prehn, S., Toetenel, W.J. (eds.), VDM '91, Formal Software Development Methods (Springer-Verlag, LNCS 551, 1991) pp. 547–569Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Jonathan Bowen
    • 1
  • Victoria Stavridou
    • 2
  1. 1.Oxford University Computing LaboratoryProgramming Research GroupOxfordUK
  2. 2.Department of Computer ScienceRoyal Holloway, University of LondonEghamUK

Personalised recommendations