ISBN 0-321-22862-6		55ドル.00 US cloth-bound
Addison-Wesley			82ドル.99 Canada
Pearson Education		September 2003
http://awprofessional.com	http://spinroot.com

Part I: Introduction

Preface

ix

1

Finding Bugs in Concurrent Systems

Circular Blocking, Deadly Embrace, Mismatched Assumptions, Fundamental Problems of Concurrency, Observability and Controllability.

1

2

Building Verification Models

Introducing PROMELA, Some Examples, Biographical Notes.

7

3

An Overview of PROMELA

Processes, Data Objects, Message Channels, Channel Poll Operations, Sorted Send and Random Receive, Rendezvous Communication, Rules for Executability, Control Flow, Finding out More.

33

4

Defining Correctness Claims

Basic Types of Claims, Assertions, Meta-Labels, Fair Cycles, Never Claims, The Link with LTL, Trace Assertions, Predefined Variables and Functions, Path Quantification, Finding out More.

73

5

Using Design Abstraction

What Makes a Good Design Abstraction?, Data and Control, The Smallest Sufficient Model, Avoiding Redundancy, Counters, Sinks, Sources, and Filters, Simple Refutation Models, Examples, Controlling Complexity, A Formal Basis for Reduction.

101

Part II: Foundations

6

Automata and Logic

Omega Acceptance, The Stutter Extension Rule, Finite States, Infinite Runs, Other Types of Acceptance, Temporal Logic, Recurrence and Stability, Valuation Sequences, Stutter Invariance, Fairness, From Logic to Automata, Omega-Regular Properties, Other Logics, Bibliographic Notes.

127

7

PROMELA Semantics

Transition Relation, Operational Model, Semantics Engine, Interpreting PROMELA Models, Three Examples, Verification, The Never Claim.

153

8

Search Algorithms

Depth-First Search, Checking Safety Properties, Depth-Limited Search, Trade-Offs, Breath-First Search, Checking Liveness Properties, Adding Fairness, The SPIN Implementation, Complexity Revisited, Bibliographic Notes.

167

9

Search Optimization

Partial Order Reduction, Visibility, Statement Merging, State Compression, Collapse Compression, The Minimized Automaton Representation, Bitstate Hashing, Bloom Filters, Hash-Compact, Bibliographic Notes.

191

10

Notes on Model Extraction

The Role of Abstraction, From ANSI-C to PROMELA, Embedded Assertions, A Framework for Abstraction, Soundness and Completeness, Selective Data Hiding, Bolder Abstractions, Dealing with False Negatives, Thorny Issues with Embedded C Code, The Model Extraction Process, The Halting Problem Revisited, Bibliographic Notes.

217

Part III: Practice

11

Using SPIN

SPIN Structure, Roadmap, Random Simulation, Interactive Simulation, Generating and Compiling a Verifier, Tuning a Verification Run, the Number of Reachable States, Search Depth, Cycle Detection, Inspecting Error Traces, Internal State Numbers, Special Cases, Disabling Partial Order Reduction, Boosting Performance, Separate Compilation, Lowering Verification Complexity.

245

12

Notes on XSPIN

Starting a Session with XSPIN, Menus, Syntax Checking, Property- Based Slicing, Simulation Parameters, Verification Parameters, The LTL Property Manager, The Automaton View Option.

267

13

The TimeLine Editor

An Example, Types of Events, Defining Events, Matching a Timeline, Automata Definitions, Variations on a Theme, Constraints, Timelines with One Event, Timelines with Multiple Events, The Link with LTL, Bibliographic Notes.

283

14

A Verification Model of a Telephone Switch

General Approach, Keeping it Simple, Managing Complexity, Subscriber Model, Switch Model, Remote Switches, Adding Features, Three-Way Calling.

299

15

Sample SPIN Models

The Sieve of Eratosthenes, Process Scheduling, A Client-Server Model, A Square-Root Server, Adding Interaction, Adding Assertions, A Comment Filter.

325

Part IV: Reference Material

16

PROMELA Language Reference

Grammar Rules, Special Cases, PROMELA Manual Pages, Meta Terms, Declarators, Control Flow Constructors, Basic Statements, Predefined Functions and Operators, Omissions.

363

17

Embedded C-Code

Example, Data References, Execution, Issues to Consider, Deferring File Inclusion, Manual Pages for Embedded C Code.

495

18

Overview of SPIN Options

Compile-Time Options, Simulation, Syntax-Checking, Postscript Generation, Model Checker Generation, LTL Conversion, Miscellaneous Options.

513

19

Overview of PAN Options

PAN Compile-Time Options, Tuning Partial Order Reduction, Increasing Speed, Decreasing Memory Use, Debugging PAN Verifiers, Experimental Options, PAN Run-Time Options, PAN Output Format.

527

Literature

545

Appendices

A

Automata Products

Asynchronous and Synchronous Products, Defining Atomic Sequences and Rendezvous, Expanded Asynchronous Products, Buchi Acceptance, Non-Progress, Deadlock.

553

B

The Great Debates

Branching vs Linear Time, Symbolic vs Explicit, Breadth-First vs Depth-First, Tarjan vs Nested, Events vs States, Realtime vs Timeless, Probability vs Possibility, Asynchronous vs Synchronous, Interleaving vs True Concurrency, Open vs Closed Systems.

563

C

Exercises with SPIN

Nine Basic Exercises.

573

D

Downloading SPIN

Spin, Cygwin, TimeLine Editor, Modex, Feaver, ltl2ba, eqltl

579

Tables and Figures

Index of Tables and Figures.

581

Index

Subject and Name index.

585-596

Goto Spin homepage Page last updated 28 October 2007