Model Checking

by Edmund M. Clarke, Orna Grumberg and Doron A. Peled

• ISBN13: 9780262032704
• ISBN10: 0262032708
• Format: Hardcover
• Copyright: 2000-01-07
• Publisher: Mit Pr

Summary

-- R. P. Kurshan, Distinguished Member Technical Staff, Bell Laboratories

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