ISBN 0321228626 $55.00 US clothbound AddisonWesley $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, MetaLabels, 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, OmegaRegular 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 
DepthFirst Search, Checking Safety Properties, DepthLimited Search, TradeOffs, BreathFirst 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, HashCompact, Bibliographic Notes.  191 
10 
Notes on Model Extraction 
The Role of Abstraction, From ANSIC 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, ThreeWay Calling.  299 
15 
Sample SPIN Models 
The Sieve of Eratosthenes, Process Scheduling, A ClientServer Model, A SquareRoot 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 CCode 
Example, Data References, Execution, Issues to Consider, Deferring File Inclusion, Manual Pages for Embedded C Code.  495 
18 
Overview of SPIN Options 
CompileTime Options, Simulation, SyntaxChecking, Postscript Generation, Model Checker Generation, LTL Conversion, Miscellaneous Options.  513 
19 
Overview of PAN Options 
PAN CompileTime Options, Tuning Partial Order Reduction, Increasing Speed, Decreasing Memory Use, Debugging PAN Verifiers, Experimental Options, PAN RunTime 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, NonProgress, Deadlock.  553 
B 
The Great Debates 
Branching vs Linear Time, Symbolic vs Explicit, BreadthFirst vs DepthFirst, 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.  585596 
Goto Spin homepage  Page last updated 28 October 2007 