Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Start single access now
Request access for companies
EXTENDED SEARCH
Log in
Top

Hint

Swipe to navigate through the chapters of this book

Published in:
Background Read chapter Read first chapter

2017 | OriginalPaper | Chapter

12. Formal Methods

Author : Gerard O’Regan

Published in: Concise Guide to Software Engineering

Publisher: Springer International Publishing

Log in

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Software Reliability and Dependability
next chapter Z Formal Specification Language
Footnotes
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].
 
Literature
1.
J.M. Spivey, The Z Notation. A Reference Manual. Prentice Hall International Series in Computer Science (Prentice-Hall, Inc., Upper Saddle River, 1992)
2.
M.J.D Brown, Rationale for the development of the UK Defence Standards for Safety Critical Software. COMPASS Conference, 1990
3.
M. Hinchey, J. Bowen (eds.), Applications of Formal Methods. Prentice Hall International Series in Computer Science (Prentice-Hall, Inc., Upper Saddle River, 1995)
4.
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
5.
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
6.
T. Kuhn, The Structure of Scientific Revolutions (University of Chicago Press, Chicago, 1970)
7.
S. Gerhart, D. Craighen, T. Ralston, Experience with formal methods in critical systems. IEEE Softw. 11, 21 (1994)
8.
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
9.
G. O’Regan, Mathematical Approaches to Software Quality (Springer, London, 2006
10.
D. Bjorner, C. Jones, The Vienna Development Method. The meta language. Lecture Notes in Computer Science, vol. 61 (Springer, New York, 1978)
11.
D. Bjorner, C. Jones, Formal Specification and software Development. Prentice Hall International Series in Computer Science (Prentice-Hall, Inc., Upper Saddle River, 1982)
12.
G. O’Regan, Guide to Discrete Mathematics (Springer, Switzerland, 2016)
13.
M.M.A. Airchinnigh, Conceptual Models and Computing. PhD Thesis. Department of Computer Science, University of Dublin, Trinity College, Dublin, 1990
14.
G. Polya, How to Solve It. A New Aspect of Mathematical Method (Princeton University Press, Princeton, 1957)
15.
I. Lakatos, Proof and Refutations. The Logic of Mathematical Discovery (Cambridge University Press, Cambridge, 1976)
16.
E. McDonnell, MSc Thesis. Department of Computer Science, Trinity College, Dublin, 1994
17.
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)
18.
D. Gries, The Science of Programming (Springer, Berlin, 1981)
19.
C.A.R. Hoare, Communicating Sequential Processes. Prentice Hall International Series in Computer Science (Prentice-Hall, Inc., Upper Saddle River, 1985)
20.
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
21.
B.A. Wickmann, A Personal View of Formal Methods. National Physical Laboratory, 2000
Metadata
Title
Formal Methods
Author
Gerard O’Regan
Copyright Year
2017
Book
Concise Guide to Software Engineering

Print ISBN: 978-3-319-57749-4

Electronic ISBN: 978-3-319-57750-0

Copyright Year: 2017

DOI
https://doi.org/10.1007/978-3-319-57750-0_12

Premium Partner

    Image Credits