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. |
|
2 |
Building Verification Models |
Introducing PROMELA, Some Examples, Biographical Notes. |
|
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 |