The SPIN MODEL CHECKER -- Primer and Reference Manual

The SPIN MODEL CHECKER

Primer and Reference Manual

[book cover] 

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
Online ordering:
Related:

Table of Contents:

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