Model Checking / Edition 1

Model Checking / Edition 1

by Edmund M. Clarke Jr., Orna Grumberg, Doron Peled
     
 

ISBN-10: 0262032708

ISBN-13: 9780262032704

Pub. Date: 01/07/2000

Publisher: MIT Press

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

…  See more details below

Overview

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 1998 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.

The MIT Press

Read More

Product Details

ISBN-13:
9780262032704
Publisher:
MIT Press
Publication date:
01/07/2000
Edition description:
New Edition
Pages:
330
Product dimensions:
7.00(w) x 9.00(h) x 0.68(d)
Age Range:
18 Years

Table of Contents

Foreword 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.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 µCalculus
7.1 Introduction
7.2 The Propositional µCalculus
7.3 Evaluating FiXpoint Formulas
7.4 Representing µCalculus Formulas Using OBDDs
7.5 Translating CTL into the µ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 OntheFly Model Checking
9.6 Checking Language Containment Symbolically
10 Partial OrderReduction
10.1 Concurrency in Asynchronous Systems
10.2 Independence and Invisibility
10.3 Partial Order Reduction for LTLX
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 AssumeGuarantee 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 FiniteState 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 RealTime and Quantitative Temporal
Analysis
16.1 RealTime Systems and RateMonotonic Scheduling
16.2 Model Checking RealTime 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
References
IndeX

Read More

Customer Reviews

Average Review:

Write a Review

and post it to your social network

     

Most Helpful Customer Reviews

See all customer reviews >