Model Checking: A Tutorial Overview

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, -automata, and their relationship. Basic model checking algorithms for linear- and branching-time temporal logics are de

• Type: Conference
• Year: 2000
• Where: MOVEP
• Authors: Stephan Merz
• Keywords: Hardware, Model Checking, Model Checking Techniques, MOVEP 2000, Temporal Logics