New book: Model checking, by Clarke, Grumberg, Peled

• Subject: New book: Model checking, by Clarke, Grumberg, Peled
• From: Doron Peled <doron@research.bell-labs.com>
• Date: Mon, 24 Jan 2000 11:16:15 -0500 (EST)
• Delivered-To: cav@research.att.com
• Sender: owner-cav@research.att.com

-----------------------------New Book-------------------------------

Model Checking 
E. M. Clarke, Orna Grumberg, Doron Peled 
Mit Press ISBN: 0262032708 
Hardcover - 314 pages (December 1999) 
Price: $50.00

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. 

About the Authors:
Edmund M. Clarke, Jr., is the FORE Systems Professor of Computer
Science and Professor of Electrical and Computer Engineering at
Carnegie Mellon University. Orna Grumberg is Professor of Computer
Science at the Technion, Haifa, Israel. Doron Peled is a Member of
Technical staff at Bell Laboratories, Lucent Technologies and
an adjunct Professor at CMU.

Table of contents:

Forward by Amir Pnueli
Preface
1 Introduction
 1.1 The Need for Formal Methods
 1.2 Hardware and Software Verification
 1.3 The Process of Model Checking
 1.4 Temporal Logic and Model Checking
 1.5 Symbolic Algorithms
 1.6 Partial Order Reduction
 1.7 Other Approaches to the State Explosion Problem
2 Modeling Systems
 2.1 Modeling Concurrent Systems
 2.2 Concurrent Systems
 2.3 Example of Program Translation
3 Temporal Logics
 3.1 The Computation Tree Logic CTL*
 3.2 CTL and LTL
 3.3 Fairness
4 Model Checking
 4.1 CTL Model Checking
 4.1.1 Fairness Constraints
 4.2 LTL Model Checking by Tableau
 4.3 CTL$* Model Checking
5 Binary Decision Diagram
 5.1 Representing Boolean Formulas
 5.2 Representing Kripke Structures
6 Symbolic Model Checking
 6.1 Fixpoint Representations
 6.2 Symbolic Model Checking for CTL
 6.3 Fairness in Symbolic Model Checking
 6.4 Counterexamples and Witnesses
 6.5 An ALU Example
 6.6 Relational Product Computations
 6.7 Symbolic LTL Model Checking
7 Model Checking for the mu-calculus
 7.1 Introduction
 7.2 The Propositional mu-Calculus
 7.3 Evaluating Fixpoint Formulas
 7.4 Representing mu-Calculus formulas using OBDDs
 7.5 Translating CTL into the mu-Calculus
 7.6 Complexity Considerations
8 Model Checking in Practice
 8.1 The SMV Model Checker
 8.2 A Realistic Example
9 Model Checking and Automata Theory
 9.1 Automata on Finite and Infinite Words
 9.2 Model Checking Using Automata
 9.3 Checking Emptiness
 9.4 Translating LTL into Automata
 9.5 On-the-fly Model Checking
 9.6 Checking Language Containment Symbolically
10 Partial Order Reduction
 10.1 Concurrency in Asynchronous Systems
 10.2 Independence and Invisibility
 10.3 Partial Order Reduction for LTL-X
 10.4 An Example
 10.5 Calculating Ample Sets
 10.6 Correctness of the Algorithm
 10.7 Partial Order Reduction in SPIN
11 Equivalences and Preorders Between Structures
 11.1 Equivalence and Preorder Algorithms
 11.2 Tableau Construction
12 Compositional Reasoning
 12.1 Composition of Structures
 12.2 Justifying Assume-Guarantee Proofs
 12.3 Verifying a CPU Controller
13 Abstraction
 13.1 Cone of Influence Reduction
 13.2 Data Abstraction
14 Symmetry
 14.1 Groups and Symmetry
 14.2 Quotient Models
 14.3 Model Checking with Symmetry
 14.4 Complexity Issues
 14.5 Empirical Results
15 Infinite Families of Finite-State Systems
 15.1 Temporal Logic for Infinite Families
 15.2 Invariants
 15.3 Futurebus+ Example Reconsidered
 15.4 Graph and Network Grammars
 15.5 Undecidability Result for a Family of Token Rings
16 Discrete Real-Time and Quantitative Temporal Analysis
 16.1 Real-Time Systems and Rate-Monotonic Scheduling
 16.2 Model Checking Real-Time Systems
 16.3 RTCTL Model Checking
 16.4 Quantitative Temporal Analysis: Minimum/Maximum Delay
 16.5 Example--An Aircraft Controller
17 Continuous Real Time
 17.1 Timed Automata
 17.2 Parallel Composition
 17.3 Modeling with Timed Automata
 17.4 Clock Regions
 17.5 Clock Zones
 17.6 Difference Bound Matrices
 17.7 Complexity Considerations
18 Conclusion

• Prev: SERG REPORT - Deriving Real-Time Monitors from System Requirements Documentation
• Next: call for participation: ASM2000, March 19th - March 24th
• Index: AMAST Mail 2000