Advertisement

Formal Methods

  • Gerard O’Regan
Chapter
Part of the Undergraduate Topics in Computer Science book series (UTICS)

Abstract

The term “formal methods” refer to various mathematical techniques used for the formal specification and development of software. They consist of a formal specification language, and employ a collection of tools to support the syntax checking of the specification, as well as the proof of properties of the specification. They allow questions to be asked about what the system does independently of the implementation.

The use of mathematical notation avoids speculation about the meaning of phrases in an imprecisely worded natural language description of a system. Natural language is inherently ambiguous, whereas mathematics employs a precise rigorous notation.

Formals methods consist of a set of mathematical techniques to specify and derive a program from its specification. Formal methods may be employed to rigorously state the requirements of the proposed system; they may be employed to derive a program from its mathematical specification; and they provide a rigorous proof that the implemented program satisfies its specification. They have been mainly applied to the safety critical field.

Keywords

Formal Method Proof Obligation Communicate Sequential Process Weak Precondition Predicate Transformer 
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

  1. 5.
    Bjorner D, Cliff J (1978) The Vienna development method. The meta language, vol 61, Lecture notes in computer science. Springer, New YorkGoogle Scholar
  2. 6.
    Bjorner D, Jones C (1982) Formal specification and software development, Prentice Hall International series in computer science. Prentice Hall International, Englewood CliffsGoogle Scholar
  3. 13.
    Chrissis MB, Conrad M, Shrum S (2011) CMMI for development. Guidelines for process integration and product improvement, 3rd edn, SEI series in software engineering. Addison Wesley, BostonGoogle Scholar
  4. 25.
    Gries D (1981) The science of programming. Springer, BerlinGoogle Scholar
  5. 22.
    Gerhart S, Craighen D, Ralston T (1994) Experience with formal methods in critical systems. IEEE Software, January 1994Google Scholar
  6. 27.
    Hinchey M, Bowen J (eds) (1995) Applications of formal methods, Prentice Hall International series in computer science. Prentice Hall, New YorkGoogle Scholar
  7. 26.
    Hoare CAR (1985) Communicating sequential processes, Prentice Hall International series in computer science. Prentice Hall International, Englewood CliffsGoogle Scholar
  8. 28.
    Hoare JP (1995) Application of the B-method to CICS. In: Hinchey M, Bowen JP (eds) Applications of formal methods, Prentice Hall International series in computer science. Prentice Hall, New YorkGoogle Scholar
  9. 36.
    Kuhn T (1970) The structure of scientific revolutions. University of Chicago Press, ChicagoGoogle Scholar
  10. 37.
    Lakatos I (1976) Proof and refutations. The logic of mathematical discovery. Cambridge University Press, CambridgeGoogle Scholar
  11. 39.
    Mac An Airchinnigh M (1990) Conceptual models and computing. PhD thesis, Department of Computer Science, University of Dublin. Trinity College, DublinGoogle Scholar
  12. 43.
    McDonnell E (1994) MSc thesis. Department of computer science. Trinity College, DublinGoogle Scholar
  13. 42.
    Milner R et al (1989) A calculus of mobile processes (Part 1). LFCS report series. ECS-LFCS-89-85. Department of Computer Science. University of Edinburgh, EdinburghGoogle Scholar
  14. 44.
    Ministry of Defence (1991) 00-55 (PART 1)/Issue 1, The procurement of safety critical software in defence equipment, PART 1: Requirements. Ministry of Defence, Interim Defence Standard, UKGoogle Scholar
  15. 45.
    Ministry of Defence (1991) 00-55 (PART 2)/Issue 1, The procurement of safety critical software in defence equipment, PART 2: Guidance. Ministry of Defence, Interim Defence Standard, UKGoogle Scholar
  16. 47.
    O’Regan G (2002) A practical approach to software quality. Springer, New YorkGoogle Scholar
  17. 48.
    O’Regan G (2006) Mathematical approaches to software quality. Springer, LondonGoogle Scholar
  18. 50.
    O’Regan G (2013) Mathematics in computing. Springer, LondonGoogle Scholar
  19. 54.
    Polya G (1957) How to solve it. A new aspect of mathematical method. Princeton University Press, PrincetonGoogle Scholar
  20. 55.
    Rational for the development of the U.K. defence standards for safety critical software. COMPASS conference, June 1990. Ministry of DefenceGoogle Scholar
  21. 62.
    Spivey JM (1992) The Z notation. A reference manual, Prentice Hall International series in computer science. Prentice Hall, Englewood CliffsGoogle Scholar
  22. 65.
    Tierney M (1991) The evolution of Def Stan 00-55 and 00-56: an intensification of the “Formal Methods debate” in the UK. Research Centre for Social Sciences, University of Edinburgh, EdinburghGoogle Scholar
  23. 66.
    Wichmann BA (2000) A personal view of formal methods. National Physical Laboratory, March 2000Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Gerard O’Regan
    • 1
  1. 1.SQC ConsultingMallowIreland

Personalised recommendations