An Introduction to Model Checking

Stephan Merz

Abstract

In formal logic, model checking designates the problem of determining whether a formula F evaluates to true or false in an interpretation K. This problem finds applications in computer science: for example, K might represent a knowledge base and F could be a query of which we wish to determine if it is implied by the knowledge in the base. We are then interested in finding efficient algorithms for the model checking problem. In this chapter, we are interested in applications where K represents a system and F a formula that represents a correctness property of this system. Typically, the systems we are interested in are reactive, that is, they interact repeatedly with their environment. They are often more concerned with control than with data and are usually composed of several components operating in parallel. Starting from a simple lift control application, we present basic ideas and concepts of verification algorithms in this context.

This chapter is intended as an introduction to the fundamental concepts and techniques of algorithmic verification. It reflects a necessarily subjective reading of the (abundant) studies. We try to give many references to original work so that the chapter can be read as an annotated bibliography.

© ISTE 2008 (publisher link)

Available as: PDF

You may also be interested in the table of contents or the preface of the volume.

Reference

@InCollection{merz:modelchecking-iste,
  author = 	 {Stephan Merz},
  title = 	 {An Introduction to Model Checking},
  booktitle = 	 {Modeling and Verification of Real-Time Systems},
  pages = 	 {77--109},
  publisher = {ISTE Publishing},
  year = 	 2008,
  editor = 	 {S. Merz and N. Navet},
  address = 	 {London, UK},
}