Model Checking: A Tutorial Overview

Stephan Merz
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
  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}

Stephan Merz
Last modified: Mon Feb 17 14:17:22 MET 2003