Model Checking, 2e

by Jr., Grumberg, Kroening, Peled, Veith

ISBN: 9780262038836 | Copyright 0

Click here to preview

Instructor Requests

Digital Exam/Desk Copy Print Desk Copy Ancillaries
Tabs

An expanded and updated edition of a comprehensive presentation of the theory and practice of model checking, a technology that automates the analysis of complex systems.

Model checking is a verification technology that provides an algorithmic means of determining whether an abstract model—representing, for example, a hardware or software design—satisfies a formal specification expressed as a temporal logic formula. If the specification is not satisfied, the method identifies a counterexample execution that shows the source of the problem. Today, many major hardware and software companies use model checking in practice, for verification of VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms. This book offers a comprehensive presentation of the theory and practice of model checking, covering the foundations of the key algorithms in depth.

The field of model checking has grown dramatically since the publication of the first edition in 1999, and this second edition reflects the advances in the field. Reorganized, expanded, and updated, the new edition retains the focus on the foundations of temporal logic model while offering new chapters that cover topics that did not exist in 1999: propositional satisfiability, SAT-based model checking, counterexample-guided abstraction refinement, and software model checking. The book serves as an introduction to the field suitable for classroom use and as an essential guide for researchers.

Expand/Collapse All
Contents (pg. vii)
List of Figures (pg. xiii)
Foreword (pg. xix)
1. Introduction to the Second Edition (pg. 1)
2. Introduction to the First Edition (pg. 3)
2.1 The Need for Formal Methods (pg. 3)
2.2 Hardware and Software Verification (pg. 4)
2.3 The Process of Model Checking (pg. 6)
2.4 Temporal Logic and Model Checking (pg. 6)
2.5 Symbolic Algorithms (pg. 8)
2.6 Partial Order Reduction (pg. 10)
2.7 Other Approaches to the State Explosion Problem (pg. 11)
3. Modeling Systems (pg. 15)
3.1 Transition Systems and Kripke Structures (pg. 16)
3.2 Nondeterminism and Inputs (pg. 17)
3.3 First-Order Logic and Symbolic Representations (pg. 18)
3.4 Boolean Encoding (pg. 22)
3.5 Modeling Digital Circuits (pg. 23)
3.6 Modeling Programs (pg. 26)
3.7 Fairness (pg. 33)
4. Temporal Logic (pg. 37)
4.1 The Computation Tree Logic CTL* (pg. 37)
4.2 Syntax and Semantics of CTL* (pg. 39)
4.3 Temporal Logics Based on CTL* (pg. 43)
4.4 Temporal Logic with Set Atomic Propositions and Set Semantics (pg. 47)
4.5 Fairness (pg. 47)
4.6 Counterexamples (pg. 48)
4.7 Safety and Liveness Properties (pg. 50)
5. CTL Model Checking (pg. 53)
5.1 Explicit-State CTL Model Checking (pg. 53)
5.2 Model-Checking CTL with Fairness Constraints (pg. 58)
5.3 CTL Model Checking via Fixpoint Computation (pg. 60)
6. LTL and CTL* Model Checking (pg. 71)
6.1 The Tableau Construction (pg. 72)
6.2 LTL Model Checking with Ta (pg. 74)
6.3 Correctness Proof of the Tableau Construction (pg. 76)
6.4 CTL* Model Checking (pg. 80)
7. Automata on Infinite Words and LTL Model Checking (pg. 85)
7.1 Finite Automata on Finite Words (pg. 85)
7.2 Automata on Infinite Words (pg. 87)
7.3 Deterministic versus Nondeterministic Büchi Automata (pg. 88)
7.4 Intersection of Büchi Automata (pg. 89)
7.5 Checking Emptiness (pg. 91)
7.6 Generalized Büchi Automata (pg. 95)
7.7 Automata and Kripke Structures (pg. 96)
7.8 Model Checking using Automata (pg. 97)
7.9 From LTL to Büchi Automata (pg. 98)
7.10 Efficient Translation of LTL into Automata (pg. 100)
7.11 On-the-Fly Model Checking (pg. 108)
8. Binary Decision Diagrams and Symbolic Model Checking (pg. 113)
8.1 Representing Boolean Formulas (pg. 113)
8.2 Representing Kripke Structures with OBDDs (pg. 119)
8.3 Symbolic Model Checking for CTL (pg. 121)
8.4 Fairness in Symbolic Model Checking (pg. 124)
8.5 Counterexamples and Witnesses (pg. 125)
8.6 Relational Product Computations (pg. 128)
9. Propositional Satisfiability (pg. 137)
9.1 Conjunctive Normal Form (pg. 137)
9.2 Encoding Propositional Logic into CNF (pg. 139)
9.3 Propositional Satisfiability using Binary Search (pg. 140)
9.4 Boolean Constraint Propagation (BCP) (pg. 144)
9.5 Conflict-Driven Clause Learning (pg. 145)
9.6 Decision Heuristics (pg. 148)
10. SAT-Based Model Checking (pg. 153)
10.1 Bounded Model Checking (pg. 153)
10.2 Verifying Reachability Properties with k-Induction (pg. 161)
10.3 Model Checking with Inductive Invariants (pg. 164)
10.4 Model Checking with Craig Interpolants (pg. 165)
10.5 Property-Directed Reachability (pg. 170)
11. Equivalences and Preorders between Structures (pg. 177)
11.1 Bisimulation Equivalence (pg. 177)
11.2 Fair Bisimulation (pg. 182)
11.3 Preorders between Structures (pg. 182)
11.4 Games for Bisimulation and Simulation (pg. 185)
11.5 Equivalence and Preorder Algorithms (pg. 186)
12. Partial Order Reduction (pg. 189)
12.1 Concurrency in Asynchronous Systems (pg. 190)
12.2 Independence and Invisibility (pg. 192)
12.3 Partial Order Reduction for LTL_X (pg. 195)
12.4 An Example (pg. 199)
12.5 Calculating Ample Sets (pg. 202)
12.6 Correctness of the Algorithm (pg. 207)
12.7 Partial Order Reduction in SPIN (pg. 211)
13. Abstraction (pg. 219)
13.1 Existential Abstraction (pg. 220)
13.2 Computation of Abstract Models (pg. 226)
13.3 Counterexample-Guided Abstraction Refinement (CEGAR) (pg. 231)
14. Software Model Checking (pg. 241)
14.1 Representing Programs as Control-Flow Graphs (pg. 241)
14.2 Checking Assertions using Symbolic Execution (pg. 242)
14.3 Program Verification with Predicate Abstraction (pg. 244)
14.4 A Full Example (pg. 248)
15. Verification with Automata Learning (pg. 257)
15.1 Angluin’s L* Learning Algorithm (pg. 257)
15.2 Compositional Reasoning (pg. 260)
15.3 Assume-Guarantee Reasoning for Communicating Components (pg. 262)
15.4 Black Box Checking (pg. 270)
16. Model Checking for the μ-Calculus (pg. 277)
16.1 Introduction (pg. 277)
16.2 The Propositional μ-Calculus (pg. 277)
16.3 Evaluating Fixpoint Formulas (pg. 281)
16.4 Representing μ-Calculus Formulas using OBDDs (pg. 284)
16.5 Translating CTL into the μ-Calculus (pg. 287)
17. Symmetry (pg. 291)
17.1 Groups and Symmetry (pg. 291)
17.2 Quotient Models (pg. 294)
17.3 Model Checking with Symmetry (pg. 297)
17.4 Complexity Issues (pg. 299)
17.5 Empirical Results (pg. 303)
18. Infinite Families of Finite-State Systems (pg. 307)
18.1 Temporal Logic for Infinite Families (pg. 307)
18.2 Invariants (pg. 308)
18.3 Futurebus+ Example Reconsidered (pg. 310)
18.4 Graph and Network Grammars (pg. 313)
18.5 Undecidability Result for a Family of Token Rings (pg. 323)
19. Discrete Real-Time and Quantitative Temporal Analysis (pg. 329)
19.1 Real-Time Systems and Rate-Monotonic Scheduling (pg. 329)
19.2 Model-Checking Real-Time Systems (pg. 330)
19.3 RTCTL Model Checking (pg. 331)
19.4 Quantitative Temporal Analysis: Minimum/Maximum Delay (pg. 332)
19.5 Example: An Aircraft Controller (pg. 335)
20. Continuous Real Time (pg. 341)
20.1 Timed Automata (pg. 342)
20.2 Parallel Composition (pg. 344)
20.3 Modeling with Timed Automata (pg. 345)
20.4 Clock Regions (pg. 346)
20.5 Clock Zones (pg. 354)
20.6 Difference-Bound Matrices (pg. 360)
20.7 Complexity Considerations (pg. 364)
Bibliography (pg. 367)
Index (pg. 399)

Edmund M. Clarke Jr.

Edmund M. Clark, Jr., is Professor of Computer Science at Carnegie Mellon University.

Orna Grumberg

. Orna Grumberg is Professor of Computer Science at Technion, Israel Institute of Technology.

Daniel Kroening

Daniel Kroening is Professor of Computer Science at the University of Oxford.

Doron Peled

Doron Peled is Professor of Computer Science at Bar-Ilan University.

Helmut Veith

Helmut Veith was a Professor on the Faculty of Informatics at Vienna University of Technology (TU Vienna).

eTextbook
Go paperless today! Available online anytime, nothing to download or install.

Features

  • Bookmarking
  • Note taking
  • Highlighting