Systems and Software Verification: Model-Checking Techniques and Tools

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