Unfoldings: A Partial-Order Approach to Model Checking / Edition 1

Unfoldings: A Partial-Order Approach to Model Checking / Edition 1

ISBN-10:
3540774254
ISBN-13:
9783540774259
Pub. Date:
04/28/2008
Publisher:
Springer Berlin Heidelberg

Hardcover

Current price is , Original price is $139.99. You
Select a Purchase Option (2008)
  • purchase options
    $111.99 $139.99 Save 20% Current price is $111.99, Original price is $139.99. You Save 20%.
  • purchase options

Overview

Unfoldings: A Partial-Order Approach to Model Checking / Edition 1

Model checking is a prominent technique used in the hardware and software industries for automatic verification. While it is very successful in finding subtle bugs in distributed systems, it faces the state explosion problem - the number of reachable states grows exponentially in the number of concurrent components.

In this book the authors introduce unfoldings, an approach to model checking which alleviates the state explosion problem by means of concurrency theory. They offer a gentle introduction to the basics of the method, and in particular they detail an unfolding-based algorithm for model checking concurrent systems against properties specified as formulas of linear temporal logic (LTL). Self-contained chapters cover transition systems and their products; unfolding products; search procedures for basic verification problems, such as reachability and livelocks; and model checking LTL. The final chapter summarizes the results of the book, and points the reader to tools and case studies.

The book will be of value to researchers and graduate students engaged in automatic verification and concurrency theory.

Product Details

ISBN-13: 9783540774259
Publisher: Springer Berlin Heidelberg
Publication date: 04/28/2008
Series: Monographs in Theoretical Computer Science. An EATCS Series
Edition description: 2008
Pages: 172
Product dimensions: 6.10(w) x 9.25(h) x 0.02(d)

Table of Contents

1 Introduction 1

2 Transition Systems and Products 5

2.1 Transition Systems 5

2.2 Products of Transition Systems 6

2.3 Petri Net Representation of Products 8

2.4 Interleaving Representation of Products 10

3 Unfolding Products 13

3.1 Branching Processes and Unfoldings 14

3.2 Some Properties of Branching Processes 22

3.2.1 Branching Processes Are Synchronizations of Trees 22

3.2.2 Causality, Conflict, and Concurrency 23

3.2.3 Configurations 25

3.3 Verification Using Unfoldings 26

3.4 Constructing the Unfolding of a Product 28

3.5 Search Procedures 33

3.6 Goals and Milestones for Next Chapters 35

4 Search Procedures for the Executability Problem 41

4.1 Search Strategies for Transition Systems 41

4.2 Search Scheme for Transition Systems 43

4.3 Search Strategies for Products 48

4.3.1 Mazurkiewicz Traces 50

4.3.2 Search Strategies as Orders on Mazurkiewicz Traces 53

4.4 Search Scheme for Products 56

4.4.1 Counterexample to Completeness 58

4.5 Adequate Search Strategies 59

4.5.1 The Size and Parikh Strategies 63

4.5.2 Distributed Strategies 64

4.6 Complete Search Scheme for Arbitrary Strategies 67

5 More on the Executability Problem 73

5.1 Complete Prefixes 73

5.1.1 Some Complexity Results 76

5.1.2 Reducing Verification Problems to SAT 78

5.2 Least Representatives 82

5.3 Breadth-First and Depth-First Strategies 86

5.3.1 Total Breadth-First Strategies 86

5.3.2 Total Depth-First Strategies 86

5.4 Strategies Preserved by Extensions Are Well-Founded 91

6 Search Procedures for the Repeated Executability Problem 97

6.1 Search Scheme for Transition Systems 97

6.2 Search Scheme for Products 101

7 Search Procedures for theLivelock Problem 107

7.1 Search Scheme for Transition Systems 107

7.2 Search Scheme for Products 115

8 Model Checking LTL 125

8.1 Linear Temporal Logic 126

8.2 Interpreting LTL on Products 126

8.2.1 Extending the Interpretation 128

8.3 Testers for LTL Properties 129

8.3.1 Constructing a Tester 130

8.4 Model Checking with Testers: A First Attempt 136

8.5 Stuttering Synchronization 138

9 Summary, Applications, Extensions, and Tools 151

9.1 Looking Back: A Two-Page Summary of This Book 151

9.2 Some Experiments 152

9.3 Some Applications 153

9.4 Some Extensions 154

9.5 Some Tools 156

References 157

Index 165

Customer Reviews

Most Helpful Customer Reviews

See All Customer Reviews