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