Systems and Software Verification : Model-Checking Techniques and Tools

Model checking is a powerful approach for the formal verification of software. When applicable, it automatically provides complete proofs of correctness, or explains, via counter-examples, why a system is not correct. This book provides a basic introduction to this new technique. The first part describes in simple terms the theoretical basis of model checking: transition systems as a formal model of systems, temporal logic as a formal language for behavioral properties, and model-checking algorithms. The second part explains how to write rich and structured temporal logic specifications in practice, while the third part surveys some of the major model checkers available. Cover......Page __sk_0000.djvu Copyright......Page __sk_0002.djvu Contents......Page __sk_0007.djvu Foreword......Page __sk_0003.djvu Preface......Page __sk_0005.djvu Part I. Principles and Techniques......Page __sk_0011.djvu Introduction......Page __sk_0013.djvu 1.1 Introductory Examples......Page __sk_0015.djvu 1.2 A Few Definitions......Page __sk_0019.djvu 1.3 A Printer Manager......Page __sk_0021.djvu 1.4 A Few More Variables......Page __sk_0022.djvu 1.5 Synchronized Product......Page __sk_0024.djvu 1.6 Synchronization by Message Passing......Page __sk_0031.djvu 1.7 Synchronization by Shared Variables......Page __sk_0034.djvu 2. Temporal Logic......Page __sk_0037.djvu 2.1 The Language of Temporal Logic......Page __sk_0038.djvu 2.2 The Formal Syntax of Temporal Logic......Page __sk_0042.djvu 2.3 The Semantics of Temporal Logic......Page __sk_0043.djvu 2.4 PLTL and CTL: Two Temporal Logics......Page __sk_0045.djvu 2.5 The Expressivity of CTL*......Page __sk_0047.djvu 3.1 Model Checking CTL......Page __sk_0049.djvu 3.2 Model Checking PLTL......Page __sk_0052.djvu 3.3 The State Explosion Problem......Page __sk_0055.djvu 4.1 Symbolic Computation of State Sets......Page __sk_0057.djvu 4.2 Binary Decision Diagrams (BDD)......Page __sk_0061.djvu 4.3 Representing Automata by BDDs......Page __sk_0064.djvu 4.4 BDD-based Model Checking......Page __sk_0066.djvu 5. Timed Automata......Page __sk_0069.djvu 5.1 Description of a Timed Automaton......Page __sk_0070.djvu 5.2 Networks of Timed Automata and Synchronization......Page __sk_0072.djvu 5.3 Variants and Extensions of the Basic Model......Page __sk_0074.djvu 5.4 Timed Temporal Logic......Page __sk_0077.djvu 5.5 Timed Model Checking......Page __sk_0078.djvu Conclusion......Page __sk_0083.djvu Part II. Specifying with Temporal Logic......Page __sk_0085.djvu Introduction......Page __sk_0087.djvu 6.1 Reachability in Temporal Logic......Page __sk_0089.djvu 6.3 Computation of the Reachability Graph......Page __sk_0090.djvu 7.1 Safety Properties in Temporal Logic......Page __sk_0093.djvu 7.2 A Formal Definition......Page __sk_0094.djvu 7.3 Safety Properties in Practice......Page __sk_0096.djvu 7.4 The History Variables Method......Page __sk_0097.djvu 8. Liveness Properties......Page __sk_0101.djvu 8.2 Are Liveness Properties Useful?......Page __sk_0102.djvu 8.3 Liveness in the Model, Liveness in the Properties......Page __sk_0104.djvu 8.4 Verification under Liveness Hypotheses......Page __sk_0106.djvu 8.5 Bounded Liveness......Page __sk_0107.djvu 9.2 Deadlock-freeness for a Given Automaton......Page __sk_0109.djvu 9.3 Beware of Abstractions!......Page __sk_0111.djvu 10.1 Fairness in Temporal Logic......Page __sk_0113.djvu 10.3 Fairness Properties and Fairness Hypotheses......Page __sk_0114.djvu 10.4 Strong Fairness and Weak Fairness......Page __sk_0116.djvu 10.5 Fairness in the Model or in the Property?......Page __sk_0117.djvu 11. Abstraction Methods......Page __sk_0119.djvu 11.3 What Can Be Proved in the Abstract Automaton?......Page __sk_0120.djvu 11.4 Abstraction on the Variables......Page __sk_0124.djvu 11.5 Abstraction by Restriction......Page __sk_0128.djvu 11.6 Observer Automata......Page __sk_0130.djvu Conclusion......Page __sk_0135.djvu Part III. Some Tools......Page __sk_0137.djvu Introduction......Page __sk_0139.djvu 12.2 SMV's Essentials......Page __sk_0141.djvu 12.3 Describing Automata......Page __sk_0142.djvu 12.4 Verification......Page __sk_0145.djvu 12.5 Synchronizing Automata......Page __sk_0146.djvu 12.6 Documentation and Case Studies......Page __sk_0147.djvu SMV Bibliography......Page __sk_0148.djvu 13.2 SPIN'S Essentials......Page __sk_0149.djvu 13.3 Describing Processes......Page __sk_0150.djvu 13.4 Simulating the System......Page __sk_0151.djvu 13.5 Verification......Page __sk_0152.djvu SPIN Bibliography......Page __sk_0154.djvu 14.2 DESIGN/CPN's Essentials......Page __sk_0155.djvu 14.3 Editing with DESIGN/CPN......Page __sk_0156.djvu 14.4 Simulating the Net......Page __sk_0157.djvu 14.6 Documentation and Case Studies......Page __sk_0159.djvu DESIGN/CPN Bibliography......Page __sk_0160.djvu 15.2 UPPAAL's Essentials......Page __sk_0163.djvu 15.3 Modeling Timed Systems with UPPAAL......Page __sk_0164.djvu 15.5 Verification......Page __sk_0167.djvu UPPAAL Bibliography......Page __sk_0168.djvu 16.2 KRONOS' Essentials......Page __sk_0171.djvu 16.3 Describing Automata......Page __sk_0172.djvu 16.4 Synchronized Product......Page __sk_0174.djvu 16.5 Model Checking......Page __sk_0175.djvu KRONOS Bibliography......Page __sk_0177.djvu 17.2 HYTECH's Essentials......Page __sk_0179.djvu 17.3 Describing Automata......Page __sk_0180.djvu 17.4 System Analysis......Page __sk_0182.djvu 17.5 Parametric Analysis......Page __sk_0184.djvu HYTECH Bibliography......Page __sk_0186.djvu Main Bibliography......Page __sk_0189.djvu Index......Page __sk_0193.djvu Model checking is a powerful approach for the formal verification of software. It automatically provides complete proofs of correctness, or explains, via counter-examples, why a system is not correct. Here, the author provides a well written and basic introduction to the new technique. The first part describes in simple terms the theoretical basis of model transition systems as a formal model of systems, temporal logic as a formal language for behavioral properties, and model-checking algorithms. The second part explains how to write rich and structured temporal logic specifications in practice, while the third part surveys some of the major model checkers available. "This book is the first text on model checking at a graduate/undergraduate level. It is divided into three parts. The first part is concerned with the fundamental notions (modelling with finite automata, synchronous product of automata, temporal logic, model-checking algorithms, symbolic model checking, timed systems). The second part focuses on the practical problem of writing correctness properties in temporal logic, and on different approaches to their verification. The third part reviews several model-checking tools."--Jacket