Model Checking

Description

Model checking is a technique for verifying finite state concurrent systems such as sequential circuit designs and communication protocols. It has a number of advantages over traditional approaches that are based on simulation, testing, and deductive reasoning. In particular, model checking is automatic and usually quite fast. Also, if the design contains an error, model checking will produce a counterexample that can be used to pinpoint the source of the error. The method, which was awarded the 1999 ACM Paris Kanellakis Award for Theory and Practice, has been used successfully in practice to verify real industrial designs, and companies are beginning to market commercial model checkers. The main challenge in model checking is dealing with the state space explosion problem. This problem occurs in systems with many components that can interact with each other or systems with data structures that can assume many different values. In such cases the number of global states can be enormous. Researchers have made considerable progress on this problem over the last ten years. This is the first comprehensive presentation of the theory and practice of model checking. The book, which includes basic as well as state-of-the-art techniques, algorithms, and tools, can be used both as an introduction to the subject and as a reference for researchers.

Table of Contents

Foreword  xi 
 Amir Pnueli
   
Preface  xiii 
 Introduction
  1 (12)
 The Need for Formal Methods
  1 (1)
 Hardware and Software Verification
  2 (2)
 The Process of Model Checking
  4 (1)
 Temporal Logic and Model Checking
  4 (2)
 Symbolic Algorithms
  6 (2)
 Partial Order Reduction
  8 (2)
 Other Approaches to the State Explosion Problem
  10 (3)
 Modeling Systems
  13 (14)
 Modeling Concurrent Systems
  14 (3)
 Concurrent Systems
  17 (7)
 Example of Program Translation
  24 (3)
 Temporal Logics
  27 (8)
 The Computation Tree Logic CTL*
  27 (3)
 CTL and LTL
  30 (2)
 Fairness
  32 (3)
 Model Checking
  35 (16)
 CTL Model Checking
  35 (6)
 LTL Model Checking
  41 (5)
 Tableau
   
 CTL* Model Checking
  46 (5)
 Binary Decision Diagram
  51 (10)
 Representing Boolean Formulas
  51 (6)
 Representing Kripke Structures
  57 (4)
 Symbolic Model Checking
  61 (36)
 Fixpoint Representations
  61 (5)
 Symbolic Model Checking for CTL
  66 (2)
 Fairness in Symbolic Model Checking
  68 (3)
 Counterexamples and Witnesses
  71 (4)
 An ALU Example
  75 (2)
 Relational Product Computations
  77 (10)
 Symbolic LTL Model Checking
  87 (10)
 Model Checking for the μ-Calculus
  97 (12)
 Introduction
  97 (1)
 The Propositional μ-Calculus
  98 (3)
 Evaluating Fixpoint Formulas
  101 (3)
 Representing μ-Calculus Formulas Using OBDDs
  104 (3)
 Translating CTL into the μ-Calculus
  107 (1)
 Complexity Considerations
  108 (1)
 Model Checking in Practice
  109 (12)
 The SMV Model Checker
  109 (3)
 A Realistic Example
  112 (9)
 Model Checking and Automata Theory
  121 (20)
 Automata on Finite and Infinite Words
  121 (2)
 Model Checking Using Automata
  123 (6)
 Checking Emptiness
  129 (3)
 Translating LTL into Automata
  132 (6)
 On-the-Fly Model Checking
  138 (1)
 Checking Language Containment Symbolically
  139 (2)
 Partial Order Reduction
  141 (30)
 Concurrency in Asynchronous Systems
  142 (2)
 Independence and Invisibility
  144 (3)
 Partial Order Reduction for LTL_x
  147 (4)
 An Example
  151 (3)
 Calculating Ample Sets
  154 (6)
 Correctness of the Algorithm
  160 (4)
 Partial Order Reduction in SPIN
  164 (7)
 Equivalences and Preorders between Structures
  171 (14)
 Equivalence and Preorder Algorithms
  178 (2)
 Tableau Construction
  180 (5)
 Compositional Reasoning
  185 (8)
 Composition of Structures
  187 (2)
 Justifying Assume-Guarantee Proofs
  189 (1)
 Verifying a CPU Controller
  190 (3)
 Abstraction
  193 (22)
 Cone of Influence Reduction
  193 (2)
 Data Abstraction
  195 (20)
 Symmetry
  215 (16)
 Groups and Symmetry
  215 (3)
 Quotient Models
  218 (3)
 Model Checking with Symmetry
  221 (3)
 Complexity Issues
  224 (4)
 Empirical Results
  228 (3)
 Infinite Families of Finite-State Systems
  231 (22)
 Temporal Logic for Infinite Families
  231 (1)
 Invariants
  232 (3)
 Futurebus+ Example Reconsidered
  235 (3)
 Graph and Network Grammars
  238 (10)
 Undecidability Result for a Family of Token Rings
  248 (5)
 Discrete Real-Time and Quantitative Temporal Analysis
  253 (12)
 Real-Time Systems and Rate-Monotonic Scheduling
  253 (1)
 Model Checking Real-Time Systems
  254 (1)
 RTCTL Model Checking
  255 (1)
 Quantitative Temporal Analysis: Minimum/Maximum Delay
  256 (3)
 Example: An Aircraft Controller
  259 (6)
 Continuous Real Time
  265 (28)
 Timed Automata
  265 (3)
 Parallel Composition
  268 (1)
 Modeling with Timed Automata
  269 (5)
 Clock Regions
  274 (6)
 Clock Zones
  280 (7)
 Difference Bound Matrices
  287 (4)
 Complexity Considerations
  291 (2)
 Conclusion
  293 (4)
References  297 (12)
Index  309