Model Checking: A Tutorial Overview

Stephan Merz

Abstract

We survey principles of model checking techniques for the automatic analysis of reactive systems. The use of model checking is exemplified by an analysis of the Needham-Schroeder public key protocol. We then formally define transition systems, temporal logic, omega-automata, and their relationship. Basic model checking algorithms for linear- and branching-time temporal logics are defined, followed by an introduction to symbolic model checking and partial-order reduction techniques. The paper ends with a list of references to some more advanced topics.

© Springer-Verlag 2001

Available as:  PDF

Needham-Schroeder protocol:  Spin model, LTL properties

Reference

@InCollection{merz:model-checking,
  author = 	 {Stephan Merz},
  title = 	 {Model Checking: A Tutorial Overview},
  booktitle = 	 {Modeling and Verification of Parallel Processes},
  pages =	 {3--38},
  publisher =	 {Springer-Verlag},
  year =	 2001,
  editor =	 {F. Cassez et al.},
  volume =	 2067,
  series =	 {Lecture Notes in Computer Science},
  address =	 {Berlin}
}