Skip to main content
SpringerLink
Log in

Formal Methods

  • Chapter
High-Integrity System Specification and Design

  • 201 Accesses

Abstract

Although they are widely cited as one of those techniques that can result in high-integrity systems [31], and are being mandated more and more in certain applications (see Part 6), formal methods remain one of the most controversial areas of current software engineering practice [119].

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
eBook
USD 16.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J.M. Spivey, The Z Notation: A Reference Manual, Prentice-Hall, Englewood Cliffs, NJ., 1989.

    MATH  Google Scholar 

  2. O.-J. Dahl, E.W. Dijkstra, and C.A.R. Hoare, Structured Programming, Academic Press, Orlando, Fla., 1972, p. 6.

    MATH  Google Scholar 

  3. C.J. Nix and B.P. Collins, “The Use of Software Engineering, Including the Z Notation, in the Development of CICS,” Quality Assurance, September 1988, pp. 103–110.

    Google Scholar 

  4. J.V. Hill, P. Robinson, and P.A. Stokes, “Safety-Critical Software in Control Systems,” in Computers and Safety, Inst. Electrical Eng., Stevenage, Herts, England, UK, 1990, pp. 92–96.

    Google Scholar 

  5. J.C.P. Woodcock, “Calculating Properties of Z Specifications,” ACM SIGSoft Software Eng. Notes, July 1989, pp. 43–54.

    Google Scholar 

  6. C.B. Jones, Systematic Software Development Using VDM, Prentice-Hall, Englewood Cliffs, NJ., 1986.

    MATH  Google Scholar 

  7. D. Gries, The Science of Programming, Springer-Verlag, New York, 1981.

    MATH  Google Scholar 

  8. G. Barrett, “Formal Methods Applied to a Floating-Point Number System,” IEEE Trans. Software Eng., May 1989, pp. 611–621.

    Google Scholar 

  9. C.A. Middleburg, “VVSL. A Language for Structured VDM Specifications,” Formal Aspects of Computing, Jan.-March 1989, pp. 115–135.

    Google Scholar 

  10. A.N. Earl et al., “Specifying a Semantic Model for Use in an Integrated Project Support Environment,” in Software-Engineering Environments, I. Sommerville, ed., Peregrinus, London, 1986, pp. 202–219.

    Google Scholar 

  11. J.A. Hall, “Seven Myths of Formal Methods,” IEEE Software, Sept. 1990, pp. 11–19.

    Google Scholar 

  12. W.W. Gibbs, “Software’s Chronic Crisis,” Scientific American, Sept. 1994, pp. 86–95.

    Google Scholar 

  13. B.W. Boehm, Software Engineering Economics, Prentice-Hall, Englewood Cliffs, N.J., 1981.

    MATH  Google Scholar 

  14. S.L. Gerhart, D. Craigen, and T. Ralston, “Experience with Formal Methods in Critical Systems,” IEEE Software, Jan. 1994, pp. 21–28.

    Google Scholar 

  15. Applications of Formal Methods, M.G. Hinchey and J.P. Bowen, eds., 1995, Prentice-Hall, Hemel Hempstead, UK. http://www.comlab.ox.ac.uk/archive/formal-methods/afm-book.html

    MATH  Google Scholar 

  16. Method Integration: Concepts and Case Studies, K. Kronlf, ed., John Wiley & Sons, New York, 1993.

    Google Scholar 

  17. L.T. Semmens, R.B. France, and T.W.G. Docker, “Integrating Structured Analysis and Formal Specification Techniques,” The Computer J., Dec. 1992, pp. 600–610.

    Google Scholar 

  18. Mechanized Reasoning and Hardware Design, C.A.R. Hoare and M.J.C. Gordon, eds., Prentice-Hall, Englewood Cliffs, N.J., 1992.

    Google Scholar 

  19. J.P. Bowen, “Formal Methods in Safety-Critical Standards,” Proc. 1993 Software Engineering Standards Symp., IEEE CS Press, Los Alamitos, Calif., 1993, pp.168–177.

    Chapter  Google Scholar 

  20. J.P. Bowen, and V. Stavridou, “Safety-Critical Systems, Formal Methods and Standards,” Software Engineering J., July 1993, pp. 189–209.

    Google Scholar 

  21. A. Dix, Formal Methods for Interactive Systems, Academic Press, San Diego, Calif., 1991.

    Google Scholar 

  22. J.V. Guttag, J.J. Horning, and J.M. Wing. Some remarks on putting formal specifications to productive use. Science of Computer Programming, North-Holland, 2(1), October 1982.

    Google Scholar 

  23. J.V. Guttag, J.J. Horning, and J.M. Wing. The Larch family of specification languages. IEEE Software, 2(5):24–36, September 1985.

    Article  Google Scholar 

  24. J.V. Guttag, J.J. Horning, and J.M. Wing. Larch in five easy pieces. Technical Report 5, DEC Systems Research Center, July 1985.

    Google Scholar 

  25. C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985.

    MATH  Google Scholar 

  26. C.B. Jones. Software Development: A Rigorous Approach. Prentice-Hall International, 1980.

    MATH  Google Scholar 

  27. C.B. Jones. Systematic Software Development Using VDM. Prentice-Hall International, 1986.

    MATH  Google Scholar 

  28. R. Koymans, J Vytopil, and W.P. de Roever. Real time programming and asynchronous message passing. In Proceedings of the 2nd ACM Symposium on Principles of Distributed Programming, pages 187–197, 1983.

    Google Scholar 

  29. L. Lamport. Specifying concurrent program modules. ACM Trans. Programming Languages and Systems (TOPLAS), 5(2): 190–222, April 1983.

    Article  MATH  Google Scholar 

  30. L. Lamport. A simple approach to specifying concurrent systems. CACM, 32(1):32–45, January 1989.

    MathSciNet  Google Scholar 

  31. B. Meyer. On formalism in specifications. IEEE Software, pages 6–26, January 1985.

    Google Scholar 

  32. A. Pnueli. Applications of temporal logic to the specification and verification of reactive systems: A survey of current trends. In W.-P. de Roever and G. Rozenberg, editors, Current Trends in Concurrency: Overviews and Tutorials, pages 510–584. Springer-Verlag, 1986. Lecture Notes in Computer Science 224.

    Chapter  Google Scholar 

  33. J.M. Spivey. Introducing Z: a Specification Language and its Formal Semantics. Cambridge University Press, 1988.

    Google Scholar 

Further Reading

  • R.M. Burstall and J. A. Goguen. The semantics of Clear, a specification language. In Proceedings of the 1979 Copenhagen Winter School on Abstract Software Specification, pages 292–332. Springer-Verlag, 1980. Lecture Notes in Computer Science 86.

    Google Scholar 

  • H.-D. Ehrich. Extensions and implementations of abstract data type specifications. In Mathematical Foundations of Computer Science 1978 Proceedings, pages 155–164. Springer-Verlag, Poland, 1978. Lecture Notes in Computer Science 64.

    Chapter  Google Scholar 

  • H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1. Springer-Verlag, Berlin, 1985.

    MATH  Google Scholar 

  • K. Futatsugi, J.A. Goguen, J.-R Jouannaud, and J. Meseguer. Principles of OBJ2. In Proceedings of ACM Principles of Programming Languages (POPL), pages 52–66, 1985.

    Google Scholar 

  • J.A. Goguen, J.W. Thatcher, E.G. Wagner, and J.B. Wright. Abstract data types as initial algebras and correctness of data representations. In Proceedings of the Conference of Computer Graphics, Pattern Recognition and Data Structures, pages 89–93. ACM, May 1975.

    Google Scholar 

  • J.V Guttag. The Specification and Application to Programming of Abstract Data Types. PhD thesis, University of Toronto, Toronto, Canada, September 1975.

    Google Scholar 

  • S. Kamin. Final data types and their specification. ACM Trans. Programming Languages and Systems (TOPLAS), 5(1):97–121, January 1983.

    Article  MATH  Google Scholar 

  • D.C. Luckham and F.W. von Henke. An overview of Anna, a specification language for Ada. IEEE Software, 2(2):9–23, March 1985.

    Article  Google Scholar 

  • R. Nakajima, M. Honda, and H. Nakahara. Hierarchical program specification and verification — a many-sorted logical approach. Acta Informatica, 14:135–155, 1980.

    Article  MATH  Google Scholar 

  • L. Robinson and O. Roubine. Special — a specification and assertion language. Technical Report CSL-46, Stanford Research Institute, Menlo Park, CA, January 1977.

    Google Scholar 

  • M. Wand. Final algebra semantics and data type extensions. Journal of Computer and System Sciences, 19(1):27–44, August 1979.

    Article  MathSciNet  MATH  Google Scholar 

  • J.M. Wing. Writing Larch interface language specifications. ACM Trans. Programming Languages and Systems (TOPLAS), pages 1–24, January 1987.

    Google Scholar 

  • S.N. Zilles. Abstract specifications for data types. IBM Research Laboratory, San Jose, CA, 1975.

    Google Scholar 

  • R. Balzer. Transformational implementation: An example. IEEE Trans. Software Eng., 7(1):3–14, January 1981.

    Article  Google Scholar 

  • F.L. Bauer et al. The Munich Project CIP, Volume 1: The Wide Spectrum Language CIP-L, Lecture Notes in Computer Science 183. Springer-Verlag, 1985.

    Google Scholar 

  • R.M. Burstall and J. Darlington. A transformation system for developing recursive programs. Journal of the ACM, 24(1):44–67, January 1977.

    Article  MathSciNet  MATH  Google Scholar 

  • R. Constable et al. Implementing Mathematics with the NuPRL Proof Development Environment. Prentice-Hall, 1986.

    Google Scholar 

  • E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.

    MATH  Google Scholar 

  • A. T. Goldberg. Knowledge-based programming: A survey of program design and construction techniques. IEEE Trans. Software Eng., 12(7):752–768, 1986.

    Google Scholar 

  • C.A.R. Hoare. Notes on Data Structuring, pages 83–174. Academic Press, 1972.

    Google Scholar 

  • C.A.R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(1):271–281, 1972.

    Article  MATH  Google Scholar 

  • P. Lee, F. Pfenning, G. Rollins, and W. Scherlis. The Ergo Support System: An integrated set of tools for prototyping integrated environments. In Proceedings of the Third ACM SIGSOFT Symposium on Software Development Environments, Boston, MA, pages 25–34, November 1988.

    Chapter  Google Scholar 

  • Z. Manna and R. Waldinger. A deductive approach to program synthesis. ACM Trans. Programming Languages and Systems (TOPLAS), 2(1):90–121, January 1980.

    Article  MATH  Google Scholar 

  • P. Martin-Löf. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153–175. North-Holland, Amsterdam, 1973.

    Google Scholar 

  • D. Sannella and A. Tarlecki. Program specification and development in Standard ML. In Proceedings of the Symposium on Principles of Programming Languages, pages 67–77, 1985.

    Google Scholar 

  • W.L. Scherlis and D. Scott. First steps toward inferential programming. In Proceedings of IFIPS’83, Paris, pages 199–212, 1983.

    Google Scholar 

  • K.R. Apt, N. Francez, and W.P. de Roever. A proof system for Communicating Sequential Processes. ACM Trans. Programming Languages and Systems (TOPLAS), 2(3):359–385, July 1980.

    Article  MATH  Google Scholar 

  • M. Broy. A fixed point to applicative multiprogramming. In M. Broy and G. Schmidt, editors, Theoretical Foundations of Programming Methodology, pages 565–623. Reidel Publishing Company, 1982.

    Google Scholar 

  • K.M. Chandy and J. Misra. Parallel Program Design. Addison-Wesley, 1988.

    MATH  Google Scholar 

  • M. Feather. Language support for the specification and development of composite systems. ACM Trans. on Prog. Lang., 9(2): 198–234, April 1987.

    Article  Google Scholar 

  • D. Harel. On visual formalisms. CACM, 31(5):514–530, 1988.

    MathSciNet  Google Scholar 

  • Information systems processing — open systems interconnection — LOTOS. Technical Report, International Standards Organization, 1987.

    Google Scholar 

  • N. Lynch and M. Tuttle. Hierarchical correctness proofs for distributed algorithms. Technical Report, MIT Laboratory for Computer Science, Cambridge, MA, April 1987.

    Google Scholar 

  • Z. Manna and A. Pnueli. Verification of concurrent programs, part 1: The temporal framework. Technical Report STAN-CS-81–836, Dept. of Computer Science, Stanford University, CA, June 1981.

    Google Scholar 

  • A.J.R.G. Milner. A Calculus of Communicating Systems, Lecture Notes in Computer Science 92. Springer-Verlag, 1980.

    Book  MATH  Google Scholar 

  • M. Nielsen, K. Havelund, K.R. Wagner, and C. George. The RAISE language, method, and tools. Formal Aspects of Computing, 1:85–114, 1989.

    Article  Google Scholar 

  • S. Owicki and D. Gries. Verifying properties of parallel programs: An axiomatic approach. CACM, 19(5):279–285, May 1976.

    MathSciNet  MATH  Google Scholar 

  • S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACM Trans. Programming Languages and Systems (TOPLAS), 4(3):455–495, July 1982.

    Article  MATH  Google Scholar 

  • J.L. Peterson. Petri nets. Computing Surveys, 9(3), September 1977.

    Google Scholar 

  • V Pratt. Modeling concurrency with partial orders. International Journal of Parallel Programming, 15(1):33–71, February 1986.

    Article  MathSciNet  MATH  Google Scholar 

  • P. Zave. An operational approach to requirements specification for embedded systems. IEEE Trans. Software Eng., 8(3):250–269, May 1972.

    Article  Google Scholar 

  • J.-R. Abrial. Busermanual. Technical Report, Programming Research Group, Oxford University, 1988.

    Google Scholar 

  • R. S. Boyer and J S. Moore. A Computational Logic. Academic Press, New York, 1979. ACM monograph series.

    MATH  Google Scholar 

  • E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Programming Languages and Systems (TOPLAS), 8(2):244–263, 1986.

    Article  MATH  Google Scholar 

  • - D. Craigen, S. Kromodimoeljo, I. Meisels, A. Neilson, B. Pase, and M. Saaltink. m-EVES: A tool for verifying software. In Proceedings of the 10th IEEE International Conference on Software Engineering, Singapore, April 1988. IEEE CS Press, Los Alamitos, CA, pages 324–333.

    Google Scholar 

  • S.J. Garland and J.V. Guttag. An overview of LP, the Larch Prover. In Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, Chapel-Hill, NC, pages 137–151, 1989.

    Google Scholar 

  • J.A. Goguen. OBJ as a theorem prover with applications to hardware verification. Technical Report SRI-CSL-88–4R2, Stanford Research Institute, Menlo Park, CA, August 1988.

    Google Scholar 

  • D.I. Good, R.L. London, and W.W. Bledsoe. An interactive program verification system. IEEE Trans. Software Eng., 1(1):59–67, 1979.

    Google Scholar 

  • M. Gordon. HOL: A proof-generating system for higher-order logic. In VLSI Specification, Verification and Synthesis. Kluwer, 1987.

    Google Scholar 

  • M. J. Gordon, A. J. Milner, and C. P. Wadsworth. Edinburgh LCF, Lecture Notes in Computer Science 78. Springer-Verlag, 1979.

    Google Scholar 

  • D. Harel, H. Lachover, A. Naamad, A. Pnueli, M. Politi, R. Sherman, and A. Shtul-Trauring. Statemate: A working environment for the development of complex reactive systems. In Proceedings of the 10th IEEE International Conference on Software Engineering, Singapore, April 1988. IEEE CS Press, Los Alamitos, CA.

    Google Scholar 

  • D. Kapur and D. Musser. Proof by consistency. Artificial Intelligence, 31:125–157, 1987.

    Article  MathSciNet  MATH  Google Scholar 

  • R.A. Kemmerer and S.T Eckmann. A user’s manual for the unisex system. Technical Report, Dept. of Computer Science, Univ. Calif., Santa Barbara, CA, December 1983.

    Google Scholar 

  • P. Lescanne. Computer experiments with the REVE term rewriting system generator. In Proceedings of the 10th Symposium on Principles of Programming Languages, pages 99–108, Austin, Texas, January 1983.

    Google Scholar 

  • K.N. Levitt, L. Robinson, and B.A. Silverberg. The HDM handbook. Technical Report Volumes 1–3, SRI International, Menlo Park, CA, 1979.

    Google Scholar 

  • R. Locasso, J. Scheid, D.V Schorre, and P.R. Eggert. The Ina Jo reference manual. Technical Report TM-(L)-6021/001/000, System Development Corporation, Santa Monica, CA, 1980.

    Google Scholar 

  • PR. McMullin and J.D. Gannon. Combining testing with formal specifications: A case study. IEEE Trans. on Software Eng., 9(3), May 1983.

    Google Scholar 

  • D.S. Rosenblum and D.C. Luckham. Testing the correctness of tasking supervisors with TSL specifications. In Proceedings of the ACM SIGSOFT’89 3rd Symposium on Software Testing, Analysis, and Verification (TAV-3), pages 187–196, Key West, FL, 1989.

    Chapter  Google Scholar 

  • W.R. Bevier. A verified operating system kernel. Technical Report 11, Computational Logic, Inc., March 1987.

    Google Scholar 

  • M.C. Browne, E.M. Clarke, and D. Dill. Checking the correctness of sequential circuits. In Proceedings of the IEEE International Conference on Computer Design, pages 545–548, 1985.

    Google Scholar 

  • M. Burrows, M. Abadi, and R. Needham. A logic of authentication. In Proceedings of the Symposium on Operating Systems, 1989.

    Google Scholar 

  • E.M. Clarke and O. Grumberg. Research on automatic verification of finite-state concurrent systems. Ann. Rev. Comput. Sci., 2:269–290, 1987.

    Article  MathSciNet  Google Scholar 

  • B.R Collins, J.E. Nicholls, and LH. Sorensen. Introducing formal methods: the CICS experience with Z. Technical Report TR 12.260, IBM, United Kingdom Laboratories, Hursley, 1987.

    Google Scholar 

  • W.J. Cullyer. Implementing safety-critical systems: The Viper microprocessor. In VLSI Specification, Verification and Synthesis. Kluwer, 1987.

    Google Scholar 

  • N. Delisle and D. Garlan. Formally specifying electronic instruments. In Proceedings of the Fifth International Workshop on Software Specification and Design, pages 242–248, Pittsburgh, 1989.

    Chapter  Google Scholar 

  • S.J. Garland, J.V. Guttag, and J. Staunstrup. Verification of VLSI circuits using LP. In Proceedings of the IFIP WG 10.2, The Fusion of Hardware Design and Verification. North-Holland, 1988.

    Google Scholar 

  • A. Heydon, M. Maimone, J.D. Tygar, J.M. Wing, and A. Moormann Zaremski. Constraining pictures with pictures. In Proceedings of IFIPS′89, San Francisco, August 1989.

    Google Scholar 

  • W.A. Hunt. The mechanical verification of a microprocessor design. Technical Report 6, Computational Logic, Inc., 1987.

    Google Scholar 

  • A.P Moore. Investigating formal specification and verification techniques for COMSEC software security. In Proceedings of the 1988 National Computer Security Conference, October 1988.

    Google Scholar 

  • P. Narendran and J. Stillman. Formal verification of the sobel image processing chip. In G. Birtwistle and P.A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 92–127. Springer-Verlag, 1989.

    Chapter  Google Scholar 

  • J.C.P. Woodcock. Transaction processing primitives and CSP. IBM Journal of Research and Development, 31(5):535–45, 1987.

    Article  MATH  Google Scholar 

  • M. Alford. SREM at the age of eight: The distributed computing design system. Computer, 18(4):36–46, April 1985.

    Article  Google Scholar 

  • F. DeRemer and H.H. Kron. Programming-in-the-large versus programming-in-the-small. IEEE Trans. on Software Eng., June 1976.

    Google Scholar 

  • S. Fickas. Automating the analysis process: An example. In Proceedings of the Fourth International Workshop on Software Specification and Design, pages 79–86, April 1987.

    Google Scholar 

  • M.A. Jackson. Principles of Program Design. Academic Press, London, 1975.

    Google Scholar 

  • H. Katzan. Systems Design and Documentation: An Introduction to the HIPO Method. Van Nostrand Reinhold, New York, 1976.

    Google Scholar 

  • N.G. Leveson. Software safety: What, why, and how. ACM Computing Surveys, 18(2): 125–163, June 1986.

    Article  Google Scholar 

  • D.L. Parnas. A technique for software module specification with examples. CACM, 15(5):330–336, May 1972.

    Google Scholar 

  • C. Rich, R.C. Waters, and H.B. Reubenstein. Toward a requirements apprentice. In Proceedings of the Fourth International Workshop on Software Specification and Design, pages 79–86, April 1987.

    Google Scholar 

  • W. Swartout. The Gist behavior explainer. In Proceedings of the American Association Artificial Intelligence Conference, pages 402–407, August 1983.

    Google Scholar 

  • E. Yourdon and L.L. Constantine. Structured Design: Fundamentals of a Discipline of Computer Programs and Systems Design. Yourdon Press, New York, 1978.

    Google Scholar 

Bibliography 1. Requirements

  • Specification Case Studies, Ian Hayes, ed., Prentice-Hall International, U.K., 1987.

    Google Scholar 

Bibliography 2. Logic programming

  • R. Kowalski, Logic for Problem Solving, North Holland, Amsterdam, 1979.

    MATH  Google Scholar 

  • K. L. Clark and F. G. McCabe, micro Prolog: Programming in Logic, Prentice-Hall International, U.K., 1984.

    Google Scholar 

Bibliography 3. Algebra

  • J. J. Martin, Data Types and Data Structures, Prentice-Hall International, U.K., 1986.

    MATH  Google Scholar 

Bibliography 4. Functional programming

  • P. Henderson, Functional Programming: Application and Implementation, Prentice-Hall International, U.K., 1980.

    MATH  Google Scholar 

  • H. Abelson and G. J. Sussman, Structure and Interpretation of Computer Programs, MIT Press, Cambridge, Mass., 1985.

    Google Scholar 

Bibliography 5. Procedural programming

  • D. Gries, The Science of Programming, Springer-Verlag, New York, 1981.

    MATH  Google Scholar 

  • R. C. Backhouse, Program Construction and Verification, Prentice-Hall International, U.K., 1987.

    Google Scholar 

Bibliography 6. Data refinement

  • C. B. Jones, Systematic Software Development Using WDM, Prentice-Hall International, U.K., 1986.

    Google Scholar 

Bibliography 7. Parallel programming

  • C. A. R. Hoare, Communicating Sequential Processes, Prentice-Hall International, U.K., 1985.

    MATH  Google Scholar 

  • K. M. Chandy and J. Misra, Parallel Program Design: a Foundation, Addison-Wesley, Reading, Mass., 1988.

    MATH  Google Scholar 

Bibliography 8. Computational complexity

  • A. V. Aho, J. E. Hopcroft, and J. D. Ullman, The Design and Analysis of Computer Algorithms, Addison-Wesley, Reading, Mass., 1974.

    MATH  Google Scholar 

Bibliography 9. General

  • Programming Methodology, D. Gries, ed., Springer-Verlag, New York, 1978.

    MATH  Google Scholar 

References

  1. IP. Bowen, “Formal Methods in Safety-Critical Standards,” Proc. SESS 93, Software Eng. Standards Symp., IEEE CS Press, Los Alamitos, Calif., Order No. 4240, 1993, pp. 168–177.

    Google Scholar 

  2. J.P. Bowen, and V. Stavridou, “Safety-Critical Systems, Formal Methods, and Standards,” IEE/BCS Software Eng. J., Vol. 8, No. 4, July 1993, pp. 189–209.

    Article  Google Scholar 

  3. J.P. Bowen, and M.G. Hinchey, “Formal Methods and Safety-Critical Standards,” Computer, Vol. 27, No. 8, Aug. 1994, pp. 68–71.

    Google Scholar 

  4. J.P. Bowen, and V Stavridou, “The Industrial Take-up of Formal Methods in Safety-Critical and Other Areas: A Perspective,” Proc. FME 93, First Formal Methods Europe Symp., in Lecture Notes in Computer Science, J.C.P. Woodcock and P.G. Larsen, eds., Vol. 670, Springer-Verlag, Berlin and London, pp. 183–195.

    Google Scholar 

  5. J.A. Hall, “Seven Myths of Formal Methods,” IEEE Software, Vol. 7, No. 5, Sept. 1990, pp. 11–19.

    Article  Google Scholar 

  6. J.P. Bowen, and M.G. Hinchey, “Seven More Myths of Formal Methods,” IEEE Software, Tech. Report 357, University of Cambridge Computer Laboratory, Cambridge, UK, Dec. 1994; also published in IEEE Software, Vol. 12, No. 4, July 1995, pp. 34–41

    Google Scholar 

  7. J.P. Bowen, and M.G. Hinchey. “Seven More Myths of Formal Methods: Dispelling Industrial Prejudice,” in Proc. FME 94, Second Formal Methods Europe Symp., T. Denvir, M. Naftalin, and M. Bertran, eds., Lecture Notes in Computer Science, Springer-Verlag, Berlin and London, Vol. 873, 1994, pp. 105–117.

    Google Scholar 

  8. D. Craigen, S. Gerhart, and T. Ralston, An International Survey of Industrial Applications of Formal Methods, Atomic Energy Control Board of Canada, US National Institute of Standards and Technology, and US Naval Research Laboratories, NIST GCR 93/626, National Technical Information Service, 5285 Port Royal Road, Springfield, VA 22161, USA, 1993.

    Google Scholar 

  9. D. Craigen, S. Gerhart, and T. Ralston, “Formal Methods Technology Transfer: Impediments and Innovation,” Applications of Formal Methods, in Prentice Hall Int’l Series in Computer Science, M.G. Hinchey and J.P. Bowen, eds., Prentice Hall, Hemel Hempstead, UK, 1995.

    Google Scholar 

  10. J.P. Bowen, and M.G. Hinchey, “Ten Commandments of Formal Methods,” Tech. Report No. 350, Sept. 1994, Computer Laboratory, Univ. of Cambridge, Cambridge, UK.

    Google Scholar 

  11. M.G. Hinchey, and J.P. Bowen, eds., Applications of Formal Methods, Prentice Hall Int’l Series in Computer Science, Prentice Hall, Hemel Hempstead, UK, 1995.

    MATH  Google Scholar 

  12. T.C. Jones, “Reusability in Programming: A Survey of the State of the Art,” IEEE Trans. Software Eng., Vol. 10, No. 5, Sept. 1984, pp. 488–494.

    Article  Google Scholar 

Download references

Authors
  1. Anthony Hall
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jonathan P. Bowen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Michael G. Hinchey
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jeannette M. Wing
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. C. A. R. Hoare
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag London Limited

About this chapter

Cite this chapter

Hall, A., Bowen, J.P., Hinchey, M.G., Wing, J.M., Hoare, C.A.R. (1999). Formal Methods. In: High-Integrity System Specification and Design. Formal Approaches to Computing and Information Technology (FACIT). Springer, London. https://doi.org/10.1007/978-1-4471-3431-2_3

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-3431-2_3

  • Publisher Name: Springer, London

  • Print ISBN: 978-3-540-76226-3

  • Online ISBN: 978-1-4471-3431-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation