Swipe to navigate through the chapters of this book
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.
Please log in to get access to this content
The Z Notation. A Reference Manual. J.M. Spivey. Prentice Hall. International Series in Computer Science. 1992.
Rational for the development of the U.K. Defence Standards for Safety Critical software. M.J.D Brown. Compass Conference. 1990.
Applications of Formal Methods. Edited by Michael Hinchey and Jonathan Bowen. Prentice Hall International Series in Computer Science. 1995.
00-55 (Part 1)/ Issue 1. The Procurement of Safety Critical Software in Defence Equipment. Part 1: Requirements. Ministry of Defence. Interim Defence Standard. UK. 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. UK. 1991.
The Evolution of Def Stan 00-55 and 00-56. An intensification of the formal methods debate in the UK. Margaret Tierney. Research Centre for Social Sciences. University of Edinburgh. 1991.
Experience with Formal Methods in Critical Systems. Susan Gerhart, Dan Craighen and Ted Ralston. IEEE Software. January 1994.
The Structure of Scientific Revolutions. Thomas Kuhn. University of Chicago Press. 1970.
Mathematical Approaches to Software Quality. Gerard O? Regan.Springer. 2006.
The Vienna Development Method. The Meta language. Dines Bjørner and Cliff Jones. Lecture Notes in Computer Science (61). Springer Verlag. 1978.
Formal Specification and Software Development. Dines Bjørner and Cliff Jones. Prentice Hall International Series in Computer Science. 1982.
Computation Models and Computing. PhD Thesis. Mícheál Mac An Airchinnigh. Dept. of Computer Science. Trinity College Dublin.
How to Solve It. A New Aspect of Mathematical Method. Georges Polya. Princeton University Press. 1957.
Proof and Refutations. The Logic of Mathematical Discovery. Imre Lakatos. Cambridge University Press. 1976.
MSc. Thesis. Eoin McDonnell. Dept. of Computer Science. Trinity College Dublin. 1994.
The Science of Programming. David Gries. Springer Verlag. Berlin. 1981.
A Disciple of Programming. E.W. Dijkstra. Prentice Hall. 1976.
Communicating Sequential Processes. C.A.R. Hoare. Prentice Hall International Series in Computer Science. 1985.
A Calculus of Mobile Processes. Part 1. Robin Milner et al. LFCS Report Series. ECS-LFCS-89-85. Department of Computer Science. University of Edinburgh.
A Personal View of Formal Methods. B.A. Wichmann. National Physical Laboratory. March 2000.
On the Criteria to be used in Decomposing Systems into Modules. David Parnas. Communications of the ACM, 15(12). 1972.
- Formal Methods
- Springer International Publishing
- Sequence number
- Chapter number
- Chapter 18