Abstract
This chapter discusses formal methods, which consist of a set of mathematic techniques that provide an extra level of confidence in the correctness of the 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, and they may be employed to formally state the requirements of the proposed system and to derive a program from its mathematical specification. They may be employed to provide a rigorous proof that the implemented program satisfies its specification, and they have been applied mainly to the safety-critical field.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
It is questionable whether stepwise refinement is cost-effective in mainstream software engineering, as it involves rewriting a specification ad nauseum . It is time-consuming to proceed in refinement steps with significant time also required to prove that the refinement step is valid. It is more relevant to the safety-critical field. Others in the formal methods field may disagree with this position.
- 2.
The UK Defence Standards 0055 and 0056 were later revised to be less prescriptive on the use of formal methods.
- 3.
However, the resulting software was never actually deployed on the A-7 aircraft.
- 4.
This was an impressive use of mathematical techniques and it has been acknowledged that formal methods must play an important role in future developments at Darlington. However, given the time and cost involved in the software inspection of the shutdown software some managers have less enthusiasm in shifting from hardware to software controllers [7].
- 5.
The IFAD Toolbox has been renamed to VDM Tools as IFAD sold the VDM Tools to CSK in Japan.
- 6.
Many existing theorem provers are difficult to use and are for specialist use only. There is a need to improve the usability of theorem provers.
- 7.
This verification was controversial with RSRE and Charter overselling VIPER as a chip design that conforms to its formal specification.
- 8.
This position is controversial with others arguing that if correctness is defined mathematically then the mathematical definition (i.e. formal specification) is a theorem, and the task is to prove that the program satisfies the theorem. They argue that the proofs for non-trivial programs exist and that the reason why there are not many examples of such proofs is due to a lack of mathematical specifications.
- 9.
The VDM Tools are now available from the CSK Group in Japan.
- 10.
The domain in which the software is being used will influence the willingness or otherwise of the customers to become familiar with the mathematics required. There appears to be little interest in mainstream software engineering, and their perception is that formal methods are unusable. However, in there is a greater interest in the mathematical approach in the safety-critical field.
- 11.
Most customers have a very limited interest and even less willingness to use mathematics. There are exceptions to this especially in the regulated sector.
- 12.
Mathematics that is potentially useful to software engineers is discussed in [11].
References
J.M. Spivey, The Z Notation. A Reference Manual. Prentice Hall International Series in Computer Science (Prentice-Hall, Inc., Upper Saddle River, 1992)
M.J.D Brown, Rationale for the development of the UK Defence Standards for Safety Critical Software. COMPASS Conference, 1990
M. Hinchey, J. Bowen (eds.), Applications of Formal Methods. Prentice Hall International Series in Computer Science (Prentice-Hall, Inc., Upper Saddle River, 1995)
Ministry of Defence-55 (PART 1), I Issue 1, The Procurement of Safety Critical software in Defence Equipment, PART 1: Requirements. Interim Defence Standard, U.K., 1991a
Ministry of Defence-55 (PART 2), I Issue 1, The Procurement of Safety Critical software in Defence Equipment, PART 2: Guidance. Interim Defence Standard, UK., 1991b
T. Kuhn, The Structure of Scientific Revolutions (University of Chicago Press, Chicago, 1970)
S. Gerhart, D. Craighen, T. Ralston, Experience with formal methods in critical systems. IEEE Softw. 11, 21 (1994)
M. Tierney, 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, 1991
G. O’Regan, Mathematical Approaches to Software Quality (Springer, London, 2006
D. Bjorner, C. Jones, The Vienna Development Method. The meta language. Lecture Notes in Computer Science, vol. 61 (Springer, New York, 1978)
D. Bjorner, C. Jones, Formal Specification and software Development. Prentice Hall International Series in Computer Science (Prentice-Hall, Inc., Upper Saddle River, 1982)
G. O’Regan, Guide to Discrete Mathematics (Springer, Switzerland, 2016)
M.M.A. Airchinnigh, Conceptual Models and Computing. PhD Thesis. Department of Computer Science, University of Dublin, Trinity College, Dublin, 1990
G. Polya, How to Solve It. A New Aspect of Mathematical Method (Princeton University Press, Princeton, 1957)
I. Lakatos, Proof and Refutations. The Logic of Mathematical Discovery (Cambridge University Press, Cambridge, 1976)
E. McDonnell, MSc Thesis. Department of Computer Science, Trinity College, Dublin, 1994
J.P. Hoare, Application of the B-Method to CICS, in Applications of Formal Methods, ed. By M. Hinchey, J.P. Bowen. Prentice Hall International Series in Computer Science (Prentice-Hall, Inc., Upper Saddle River, 1995)
D. Gries, The Science of Programming (Springer, Berlin, 1981)
C.A.R. Hoare, Communicating Sequential Processes. Prentice Hall International Series in Computer Science (Prentice-Hall, Inc., Upper Saddle River, 1985)
R. Milner et al., A Calculus of Mobile Processes (Part 1). LFCS Report Series. ECS-LFCS-89-85. Department of Computer Science, University of Edinburgh, 1989
B.A. Wickmann, A Personal View of Formal Methods. National Physical Laboratory, 2000
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this chapter
Cite this chapter
O’Regan, G. (2017). Formal Methods. In: Concise Guide to Software Engineering. Undergraduate Topics in Computer Science. Springer, Cham. https://doi.org/10.1007/978-3-319-57750-0_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-57750-0_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-57749-4
Online ISBN: 978-3-319-57750-0
eBook Packages: Computer ScienceComputer Science (R0)