Skip to main content Accessibility help
Internet Explorer 11 is being discontinued by Microsoft in August 2021. If you have difficulties viewing the site on Internet Explorer 11 we recommend using a different browser such as Microsoft Edge, Google Chrome, Apple Safari or Mozilla Firefox.

Chapter 3: Verification by model checking

Chapter 3: Verification by model checking

pp. 172-255

Authors

, Imperial College of Science, Technology and Medicine, London, , University of Birmingham
Resources available Unlock the full potential of this textbook with additional resources. There are Instructor restricted resources available for this textbook. Explore resources
  • Add bookmark
  • Cite
  • Share

Summary

Motivation for verification

There is a great advantage in being able to verify the correctness of computer systems, whether they are hardware, software, or a combination. This is most obvious in the case of safety-critical systems, but also applies to those that are commercially critical, such as mass-produced chips, mission critical, etc. Formal verification methods have quite recently become usable by industry and there is a growing demand for professionals able to apply them. In this chapter, and the next one, we examine two applications of logics to the question of verifying the correctness of computer systems, or programs.

Formal verification techniques can be thought of as comprising three parts:

  • a framework for modelling systems, typically a description language of some sort;

  • a specification language for describing the properties to be verified;

  • a verification method to establish whether the description of a system satisfies the specification.

Approaches to verification can be classified according to the following criteria:

  1. Proof-based vs. model-based. In a proof-based approach, the system description is a set of formulas Γ (in a suitable logic) and the specification is another formula ϕ. The verification method consists of trying to find a proof that Γ ⊢ ϕ. This typically requires guidance and expertise from the user.

  2. […]

About the book

Access options

Review the options below to login to check your access.

Purchase options

eTextbook
US$73.00
Paperback
US$73.00

Have an access code?

To redeem an access code, please log in with your personal login.

If you believe you should have access to this content, please contact your institutional librarian or consult our FAQ page for further information about accessing our content.

Also available to purchase from these educational ebook suppliers