Model Checking, second edition (Cyber Physical Systems Series)

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. Series Page Title Page Copyright Dedication Table of Contents List of Figures Foreword 1. Introduction to the Second Edition 2. Introduction to the First Edition 2.1. The Need for Formal Methods 2.2. Hardware and Software Verification 2.3. The Process of Model Checking 2.4. Temporal Logic and Model Checking 2.5. Symbolic Algorithms 2.6. Partial Order Reduction 2.7. Other Approaches to the State Explosion Problem 3. Modeling Systems 3.1. Transition Systems and Kripke Structures 3.2. Nondeterminism and Inputs 3.3. First-Order Logic and Symbolic Representations 3.4. Boolean Encoding 3.5. Modeling Digital Circuits 3.6. Modeling Programs 3.7. Fairness 4. Temporal Logic 4.1. The Computation Tree Logic CTL* 4.2. Syntax and Semantics of CTL* 4.3. Temporal Logics Based on CTL* 4.4. Temporal Logic with Set Atomic Propositions and Set Semantics 4.5. Fairness 4.6. Counterexamples 4.7. Safety and Liveness Properties 5. CTL Model Checking 5.1. Explicit-State CTL Model Checking 5.2. Model-Checking CTL with Fairness Constraints 5.3. CTL Model Checking via Fixpoint Computation 6. LTL and CTL* Model Checking 6.1. The Tableau Construction 6.2. LTL Model Checking with Tableau 6.3. Correctness Proof of the Tableau Construction 6.4. CTL* Model Checking 7. Automata on Infinite Words and LTL Model Checking 7.1. Finite Automata on Finite Words 7.2. Automata on Infinite Words 7.3. Deterministic versus Nondeterministic Büchi Automata 7.4. Intersection of Büchi Automata 7.5. Checking Emptiness 7.6. Generalized Büchi Automata 7.7. Automata and Kripke Structures 7.8. Model Checking using Automata 7.9. From LTL to Büchi Automata 7.10. Efficient Translation of LTL into Automata 7.11. On-the-Fly Model Checking 8. Binary Decision Diagrams and Symbolic Model Checking 8.1. Representing Boolean Formulas 8.2. Representing Kripke Structures with OBDDs 8.3. Symbolic Model Checking for CTL 8.4. Fairness in Symbolic Model Checking 8.5. Counterexamples and Witnesses 8.6. Relational Product Computations 9. Propositional Satisfiability 9.1. Conjunctive Normal Form 9.2. Encoding Propositional Logic into CNF 9.3. Propositional Satisfiability using Binary Search 9.4. Boolean Constraint Propagation (BCP) 9.5. Conflict-Driven Clause Learning 9.6. Decision Heuristics 10. SAT-Based Model Checking 10.1. Bounded Model Checking 10.2. Verifying Reachability Properties with k-Induction 10.3. Model Checking with Inductive Invariants 10.4. Model Checking with Craig Interpolants 10.5. Property-Directed Reachability 11. Equivalences and Preorders between Structures 11.1. Bisimulation Equivalence 11.2. Fair Bisimulation 11.3. Preorders between Structures 11.4. Games for Bisimulation and Simulation 11.5. Equivalence and Preorder Algorithms 12. Partial Order Reduction 12.1. Concurrency in Asynchronous Systems 12.2. Independence and Invisibility 12.3. Partial Order Reduction for LTL−X 12.4. An Example 12.5. Calculating Ample Sets 12.6. Correctness of the Algorithm 12.7. Partial Order Reduction in SPIN 13. Abstraction 13.1. Existential Abstraction 13.2. Computation of Abstract Models 13.3. Counterexample-Guided Abstraction Refinement (CEGAR) 14. Software Model Checking 14.1. Representing Programs as Control-Flow Graphs 14.2. Checking Assertions using Symbolic Execution 14.3. Program Verification with Predicate Abstraction 14.4. A Full Example 15. Verification with Automata Learning 15.1. Angluin’s L* Learning Algorithm 15.2. Compositional Reasoning 15.3. Assume-Guarantee Reasoning for Communicating Components 15.4. Black Box Checking 16. Model Checking for the μ-Calculus 16.1. Introduction 16.2. The Propositional μ-Calculus 16.3. Evaluating Fixpoint Formulas 16.4. Representing μ-Calculus Formulas using OBDDs 16.5. Translating CTL into the μ-Calculus 17. Symmetry 17.1. Groups and Symmetry 17.2. Quotient Models 17.3. Model Checking with Symmetry 17.4. Complexity Issues 17.5. Empirical Results 18. Infinite Families of Finite-State Systems 18.1. Temporal Logic for Infinite Families 18.2. Invariants 18.3. Futurebus+ Example Reconsidered 18.4. Graph and Network Grammars 18.5. Undecidability Result for a Family of Token Rings 19. Discrete Real-Time and Quantitative Temporal Analysis 19.1. Real-Time Systems and Rate-Monotonic Scheduling 19.2. Model-Checking Real-Time Systems 19.3. RTCTL Model Checking 19.4. Quantitative Temporal Analysis: Minimum/Maximum Delay 19.5. Example: An Aircraft Controller 20. Continuous Real Time 20.1. Timed Automata 20.2. Parallel Composition 20.3. Modeling with Timed Automata 20.4. Clock Regions 20.5. Clock Zones 20.6. Difference-Bound Matrices 20.7. Complexity Considerations Bibliography Index "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"--Résumé de l'éditeur