Skip to content

Model Checking

ISBN-10: 0262032708

ISBN-13: 9780262032704

Edition: 1999

Authors: Edmund M. Clarke, Orna Grumberg, Doron Peled

List price: $75.00
Blue ribbon 30 day, 100% satisfaction guarantee!
what's this?
Rush Rewards U
Members Receive:
Carrot Coin icon
XP icon
You have reached 400 XP and carrot coins. That is the daily max!

Description:

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 as an introduction to the subject and as a reference.
Customers also bought

Book details

List price: $75.00
Copyright year: 1999
Publisher: MIT Press
Publication date: 12/20/1999
Binding: Hardcover
Pages: 334
Size: 7.25" wide x 9.25" long x 1.00" tall
Weight: 1.584
Language: English

Foreword
Preface
Introduction
The Need for Formal Methods
Hardware and Software Verification
The Process of Model Checking
Temporal Logic and Model Checking
Symbolic Algorithms
Partial Order Reduction
Other Approaches to the State Explosion Problem
Modeling Systems
Modeling Concurrent Systems
Concurrent Systems
Example of Program Translation
Temporal Logics
The Computation Tree Logic CTL
CTL and LTL
Fairness
Model Checking
CTL Model Checking
LTL Model Checking by Tableau
CTL Model Checking
Binary Decision Diagram
Representing Boolean Formulas
Representing Kripke Structures
Symbolic Model Checking
Fixpoint Representations
Symbolic Model Checking for CTL
Fairness in Symbolic Model Checking
Counterexamples and Witnesses
An ALU Example
Relational Product Computations
Symbolic LTL Model Checking
Model Checking for the [mu]-Calculus
Introduction
The Propositional [mu]-Calculus
Evaluating Fixpoint Formulas
Representing [mu]-Calculus Formulas Using OBDDs
Translating CTL into the [mu]-Calculus
Complexity Considerations
Model Checking in Practice
The SMV Model Checker
A Realistic Example
Model Checking and Automata Theory
Automata on Finite and Infinite Words
Model Checking Using Automata
Checking Emptiness
Translating LTL into Automata
On-the-Fly Model Checking
Checking Language Containment Symbolically
Partial Order Reduction
Concurrency in Asynchronous Systems
Independence and Invisibility
Partial Order Reduction for LTL[subscript -x]
An Example
Calculating Ample Sets
Correctness of the Algorithm
Partial Order Reduction in SPIN
Equivalences and Preorders between Structures
Equivalence and Preorder Algorithms
Tableau Construction
Compositional Reasoning
Composition of Structures
Justifying Assume-Guarantee Proofs
Verifying a CPU Controller
Abstraction
Cone of Influence Reduction
Data Abstraction
Symmetry
Groups and Symmetry
Quotient Models
Model Checking with Symmetry
Complexity Issues
Empirical Results
Infinite Families of Finite-State Systems
Temporal Logic for Infinite Families
Invariants
Futurebus+ Example Reconsidered
Graph and Network Grammars
Undecidability Result for a Family of Token Rings
Discrete Real-Time and Quantitative Temporal Analysis
Real-Time Systems and Rate-Monotonic Scheduling
Model Checking Real-Time Systems
RTCTL Model Checking
Quantitative Temporal Analysis: Minimum/Maximum Delay
Example: An Aircraft Controller
Continuous Real Time
Timed Automata
Parallel Composition
Modeling with Timed Automata
Clock Regions
Clock Zones
Difference Bound Matrices
Complexity Considerations
Conclusion
References
Index