Skip to main content

Get full access to Spin Model Checker, The: Primer and Reference Manual and 60K+ other titles, with a free 10-day trial of O'Reilly.

There are also live events, courses curated by job role, and more.

Start your free trial

Spin Model Checker, The: Primer and Reference Manual

Spin Model Checker, The: Primer and Reference Manual

Released September 2003

Publisher(s): Addison-Wesley Professional

ISBN: 9780321228628

Start your free trial

Book description

Master SPIN, the breakthrough tool for improving software reliability

SPIN is the world's most popular, and arguably one of the world's most powerful, tools for detecting software defects in concurrent system designs. Literally thousands of people have used SPIN since it was first introduced almost fifteen years ago. The tool has been applied to everything from the verification of complex call processing software that is used in telephone exchanges, to the validation of intricate control software for interplanetary spacecraft.

This is the most comprehensive reference guide to SPIN, written by the principal designer of the tool. It covers the tool's specification language and theoretical foundation, and gives detailed advice on methods for tackling the most complex software verification problems.

Sum Design and verify both abstract and detailed verification models of complex systems software

Sum Develop a solid understanding of the theory behind logic model checking

Sum Become an expert user of the SPIN command line interface, the Xspin graphical user interface, and the TimeLine editing tool

Sum Learn the basic theory of omega automata, linear temporal logic, depth-first and breadth-first search, search optimization, and model extraction from source code

The SPIN software was awarded the prestigious Software System Award by the Association for Computing Machinery (ACM), which previously recognized systems such as UNIX, SmallTalk, TCP/IP, Tcl/Tk, and the World Wide Web.

Table of contents

Copyright
Preface
1. Logic Model Checking
2. The SPIN Model Checker
3. Book Structure
1. Finding Bugs in Concurrent Systems
1. Circular Blocking
2. Deadly Embrace
3. Mismatched Assumptions
4. Fundamental Problems of Concurrency
2. Building Verification Models
1. SPIN
2. PROMELA
3. Examples
4. Hello World
5. Producers and Consumers
6. Extending the Example
7. Mutual Exclusion
8. Message Passing
9. In Summary
10. Bibliographic Notes
3. An Overview of PROMELA
1. Types of Objects
2. Processes
3. Provided Clauses
4. Data Objects
5. Data Structures
6. Message Channels
7. Channel Poll Operations
8. Sorted Send And Random Receive
9. Rendezvous Communication
10. Rules For Executability
11. Assignments And Expressions
12. Control Flow: Compound Statements
13. Atomic Sequences
14. Deterministic Steps
15. Selection
16. Repetition
17. Escape Sequences
18. Inline Definitions
19. Reading Input
20. Special Features
21. Finding Out More
4. Defining Correctness Claims
1. Stronger Proof
2. Basic Types of Claims
3. Basic Assertions
4. Meta Labels
  1. End States:
  2. Progress States:
5. Fair Cycles
  1. Accept States:
6. Never Claims
  1. How a Never Claim Works
7. The Link With LTL
8. Trace Assertions
9. Notrace
10. Predefined Variables and Functions
11. Remote Referencing
12. Path Quantification
13. Formalities
14. Finding Out More
5. Using Design Abstraction
1. What Makes a Good Design Abstraction?
2. Data and Control
3. The Smallest Sufficient Model
4. Avoiding Redundancy
5. Counters
6. Sinks, Sources, and Filters
7. Simple Refutation Models
8. Pathfinder
9. A Disk-Head Scheduler
10. Controlling Complexity
11. Example
12. A Formal Basis for Reduction
  1. Property 5.1 (Reduction Property)
13. Example – A File Server
14. In Summary
15. Bibliographic Notes
6. Automata and Logic
1. Automata
2. Omega Acceptance
  1. Definition 6.5 (Büchi acceptance)
3. The Stutter Extension Rule
  1. Definition 6.6 (Stutter Extension)
4. Finite States, Infinite Runs
5. Other Types of Acceptance
6. Logic
7. Temporal Logic
8. Recurrence and Stability
9. Using Temporal Logic
10. Valuation Sequences
11. Stutter Invariance
  1. Definition 6.17 (Stutter invariance)
12. Fairness
13. From Logic To Automata
14. An Example
15. Omega-Regular Properties
16. Other Logics
17. Bibliographic Notes
7. PROMELA Semantics
1. Transition Relation
2. Operational Model
3. Operational Model, Semantics Engine
4. Interpreting PROMELA Models
5. Three Examples
6. Verification
7. The Never Claim
8. Search Algorithms
1. Depth-First Search
  1. Property 8.1
2. Checking Safety Properties
3. Depth-Limited Search
4. Trade-Offs
5. Breadth-First Search
6. Checking Liveness Properties
  1. Property 8.2
7. Adding Fairness
  1. Definition 8.1 (Strong Fairness)
  2. Definition 8.2 (Weak Fairness)
8. The SPIN Implementation
9. Complexity Revisited
10. Bibliographic Notes
9. Search Optimization
1. Partial Order Reduction
2. Visibility
3. Statement Merging
4. State Compression
5. Collapse Compression
6. Minimized Automaton Representation
7. Bitstate Hashing
8. Bloom Filters
9. Hash-Compact
10. Bibliographic Notes
10. Notes on Model Extraction
1. The Role of Abstraction
2. From ANSI-C to PROMELA
3. Embedded Assertions
4. A Framework for Abstraction
5. Sound and Complete Abstraction
  1. Definition 10.1 (Logical Soundness)
  2. Definition 10.2 (Logical Completeness)
6. Selective Data Hiding
7. Example
8. Bolder Abstractions
9. Dealing With False Negatives
10. Thorny Issues With Embedded C Code
11. The Model Extraction Process
12. The Halting Problem Revisited
13. Bibliographic Notes
11. Using SPIN
1. SPIN Structure
2. Roadmap
3. Simulation
4. Random Simulation
5. Interactive Simulation
6. Guided Simulation
7. Verification
8. Generating a Verifier
9. Compiling the Verifier
10. Tuning a Verification Run
11. The Number of Reachable States
12. Search Depth
13. Cycle Detection
14. Inspecting Error Traces
15. Internal State Numbers
16. Special Cases
17. Disabling Partial Order Reduction
18. Boosting Performance
19. Separate Compilation
20. Lowering Verification Complexity
12. Notes on XSPIN
1. Starting a Session With XSPIN
2. The File Menu
3. The Edit Menu
4. The Help Menu
5. The Run Menu
6. Syntax Check
7. Property-Based Slicing
8. Set Simulation Parameters
9. (Re)Run Simulation
10. Set Verification Parameters
11. (Re)Run Verification
12. LTL Property Manager
13. The Automaton View Option
14. In Summary
13. The Timeline Editor
1. An Example
2. Types of Events
3. Defining Events
4. Matching a Timeline
5. Automata Definitions
6. Constraints
7. Variations on a Theme
8. Timelines With One Event
9. Timelines With Multiple Events
10. The Link With LTL
11. Bibliographic Notes
14. A Verification Model of a Telephone Switch
1. General Approach
2. Keep it Simple
3. Managing Complexity
4. Modeling a Switch
5. Subscriber Model
6. Switch Model
7. Remote Switches
8. Adding Features
9. Three-Way Calling
10. A Three-Way Calling Scenario
11. In Summary
15. Sample SPIN Models
1. Eratosthenes
2. Process Scheduling
3. A Client-Server Model
4. Square Roots?
5. Adding Interaction
6. Adding Assertions
7. A Comment Filter
16. PROMELA Language Reference
1. Name
2. Syntax
3. EXECUTABILITY
4. EFFECT
5. DESCRIPTION
6. Examples
7. Notes
8. See Also
9. Grammar Rules
10. Main Sections
  1. Meta Terms
  2. Declarators
  3. Control Flow
  4. Basic Statements
  5. Predefined
  6. Embedded C Code
  7. Omissions
11. Reference
12. Special Cases
  1. Simulation Only
  2. Verification Only
  3. Partial Order Reduction
13. _
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. See Also
14. _last
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
15. _nr_pr
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. See Also
16. _pid
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
17. accept
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
18. active
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
19. arrays
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
20. assert
  1. Name
  2. Syntax
  3. Executability
  4. EFFECT
  5. Description
  6. Examples
  7. Notes
  8. See Also
21. assignment
  1. Name
  2. Syntax
  3. Executability
  4. Effect
  5. Description
  6. Examples
  7. Notes
  8. See Also
22. atomic
  1. Name
  2. Syntax
  3. Effect
  4. Description
  5. Examples
  6. Notes
  7. See Also
23. break
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
24. chan
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
25. comments
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
26. cond_expr
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. See Also
27. condition
  1. Name
  2. Syntax
  3. Executability
  4. Effect
  5. Description
  6. Examples
  7. See Also
28. d_step
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
29. datatypes
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
30. do
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
31. else
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
32. empty
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
33. enabled
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
34. end
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
35. eval
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
36. false
  1. Name
  2. Syntax
  3. Description
  4. Notes
  5. See
37. float
  1. Name
  2. Description
  3. Notes
  4. See Also
38. full
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
39. goto
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
40. hidden
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
41. hierarchy
  1. Name
  2. Description
  3. See Also
42. if
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
43. init
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
44. inline
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
45. labels
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
46. len
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
47. local
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
48. ltl
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
49. macros
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
50. mtype
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
51. nempty
  1. Name
  2. Syntax
  3. Description
  4. Notes
  5. See Also
52. never
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
53. nfull
  1. Name
  2. Syntax
  3. Description
  4. Notes
  5. See Also
54. np_
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. See Also
55. pc_value
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
56. pointers
  1. Name
  2. Description
  3. See Also
57. poll
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
58. printf
  1. Name
  2. Syntax
  3. Executability
  4. Effect
  5. Description
  6. Examples
  7. Notes
  8. See Also
59. priority
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
60. probabilities
  1. Name
  2. Description
  3. See Also
61. procedures
  1. Name
  2. Description
  3. See Also
62. proctype
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
63. progress
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
64. provided
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
65. rand
  1. Name
  2. Description
  3. Notes
  4. See Also
66. real-time
  1. Name
  2. Description
  3. See Also
67. receive
  1. Name
  2. Syntax
  3. Executability
  4. Effect
  5. Description
  6. Examples
  7. See Also
68. remoterefs
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
69. run
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
70. scanf
  1. Name
  2. Description
  3. See Also
71. send
  1. Name
  2. Syntax
  3. Executability
  4. Effect
  5. Description
  6. Examples
  7. Notes
  8. See Also
72. separators
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
73. sequence
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
74. show
  1. Name
  2. Syntax
  3. Description
  4. Notes
  5. See Also
75. skip
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
76. STDIN
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
77. timeout
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
78. trace
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
79. true
  1. Name
  2. Syntax
  3. Description
  4. Notes
  5. See
80. typedef
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
81. unless
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
82. xr
  1. Name
  2. Syntax
  3. Description
  4. Examples
  5. Notes
  6. See Also
17. Embedded C Code
1. An Example
2. Data References
3. Execution
4. Issues to Consider
5. Deferring File Inclusion
6. c_code
  1. Name
  2. Syntax
  3. Executability
  4. Effect
  5. Description
  6. Examples
  7. Notes
  8. See Also
7. c_decl
  1. Name
  2. Syntax
  3. Executability
  4. Description
  5. Examples
  6. Notes
  7. See Also
8. c_expr
  1. Name
  2. Syntax
  3. Executability
  4. Effect
  5. Description
  6. Examples
  7. Notes
  8. See Also
18. Overview of SPIN Options
1. Compile-Time Options
2. Simulation Options
  1. Alphabetical Listing
    1. -B
    2. -b
    3. -c
    4. -g
    5. -i
    6. -J
    7. -jN
    8. -l
    9. -m
    10. -nN
    11. -p
    12. -qN
    13. -r
    14. -s
    15. -T
    16. -t[N]
    17. -uN
    18. -v
    19. -w
3. Syntax Checking Options
  1. -a
  2. -A
  3. -I
  4. -Z
4. Postscript Generation
  1. -M
5. Model Checker Generation
  1. -a
  2. -N file
  3. -o1
  4. -o2
  5. -o3
  6. -o4
  7. -o5
  8. -S1 and -S2
6. LTL Conversion
  1. -f formula
  2. -F file
7. Miscellaneous Options
  1. -d
  2. -C
  3. -Dxxx
  4. -Exxx
  5. -Pxxx
  6. -V
  7. -X and -Y
19. Overview of PAN Options
1. PAN Compile-Time Options
2. Basic Options
  1. -DBFS
  2. -DMEMCNT=N
  3. -DMEMLIM=N
  4. -DNOCLAIM
  5. -DNP
  6. -DON_EXIT=STRING
  7. -DPROV=file
3. Options Related to Partial Order Reduction
  1. -DNOREDUCE
  2. -DXUSAFE
4. Options Used to Increase Speed
5. Options Used to Decrease Memory Use
  1. -DBITSTATE
  2. -DHC
  3. -DCOLLAPSE
  4. -DMA=N
  5. -DSC
6. Options to Use When Prompted by PAN
  1. -DNFAIR=N
  2. -DVECTORSZ=N
7. Options for Debugging PAN Verifiers
  1. -DVERBOSE
  2. -DCHECK
  3. -DSVDUMP
  4. -DSDUMP
8. Experimental Options
  1. -DBCOMP
  2. -DCOVEST
  3. -DCTL
  4. -DGLOB_ALPHA
  5. -DHYBRID_HASH
  6. -DLC
  7. -DNIBIS
  8. -DNOCOMP
  9. -DNOSTUTTER
  10. -DNOVSZ
  11. -DOHASH
  12. -DPEG
  13. -DPRINTF
  14. -DRANDSTOR=N
  15. -DREACH
  16. -DVAR_RANGES
9. PAN Run-Time Options
  1. -A
  2. -a
  3. -b
  4. -cN
  5. -d
  6. -E
  7. -e
  8. -f
  9. -hN
  10. -i
  11. -I
  12. -J
  13. -l
  14. -mN
  15. -n
  16. -q
  17. -s
  18. -V
  19. -wN
  20. -X
  21. -Y
10. PAN Output Format
Literature
A. Automata Products
1. Asynchronous Products
  1. Definition A.1 (Asynchronous Product)
2. Encoding Atomic Sequences
3. Rendezvous
4. Synchronous Products
  1. Definition A.2 (Synchronous Product)
5. An Example
6. Non-Progress Cycles
7. Deadlock Detection
B. The Great Debates
1. Branching Time vs Linear Time
2. Symbolic Verification vs Explicit Verification
3. Breadth-First Search vs Depth-First Search
4. Tarjan Search vs Nested Search
5. Events vs States
6. Realtime Verification vs Timeless Verification
7. Probability vs Possibilty
8. Asynchronous Systems vs Synchronous Systems
9. Interleaving vs True Concurrency
10. Open vs Closed Systems
C. Exercises With SPIN
1. C.1.
2. C.2.
3. C.3.
4. C.4.
5. C.5.
6. C.6.
7. C.7.
8. C.8.
9. C.9.
D. Downloading Spin
1. LTL Conversion
2. Model Extraction
3. Timeline Editor
Tables and Figures
1. Tables
2. Figures

Product information

Title: Spin Model Checker, The: Primer and Reference Manual
Author(s):
Release date: September 2003
Publisher(s): Addison-Wesley Professional
ISBN: 9780321228628

You might also like

book

Control Systems Engineering

by S. Salivahanan

Control Systems Engineering caters to the requirements of an interdisciplinary course on Control Systems at the …

book

Verification Techniques for System-Level Design

by Masahiro Fujita, Indradeep Ghosh, Mukul Prasad

This book will explain how to verify SoC (Systems on Chip) logic designs using “formal and …

book

Control Theory Applications for Dynamic Production Systems

by Neil A. Duffie

Control Theory Applications for Dynamic Production Systems Apply the fundamental tools of linear control theory to …

book

Handbook of Automated Reasoning

by Alan J.A. Robinson, Andrei Voronkov

Handbook of Automated Reasoning

Don’t leave empty-handed

Get Mark Richards’s Software Architecture Patterns ebook to better understand how to design components—and how they should interact.

It’s yours, free.

Get it now

Cover of Software Architecture Patterns

Check it out now on O’Reilly

Dive in for free with a 10-day trial of the O’Reilly learning platform—then explore all the other resources our members count on to build skills and solve problems every day.

Start your free trial Become a member now