You are previewing Spin Model Checker, The: Primer and Reference Manual.
O'Reilly logo
Spin Model Checker, The: Primer and Reference Manual

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

    1. Copyright
    2. Preface
      1. Logic Model Checking
      2. The SPIN Model Checker
      3. Book Structure
    3. 1. Finding Bugs in Concurrent Systems
      1. Circular Blocking
      2. Deadly Embrace
      3. Mismatched Assumptions
      4. Fundamental Problems of Concurrency
    4. 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
    5. 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
    6. 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
    7. 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
    8. 6. Automata and Logic
      1. Automata
        1. Definition 6.1 (FSA)
        2. Definition 6.2 (Determinism)
        3. Definition 6.3 (Runs)
        4. Definition 6.4 (Standard acceptance)
      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
        1. Definition 6.7 (Well-Formed Temporal Formulae)
        2. Definition 6.8 (Weak Until)
        3. Definition 6.9 (Strong Until)
        4. Definition 6.10 (Always)
        5. Definition 6.11 (Eventually)
        6. Definition 6.12 (Next)
      8. Recurrence and Stability
        1. Definition 6.13
        2. Definition 6.14
        3. Definition 6.15 (Implication)
        4. Definition 6.16 (Equivalence)
      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
    9. 7. PROMELA Semantics
      1. Transition Relation
      2. Operational Model
        1. Definition 7.1 (Variable)
        2. Definition 7.2 (Message)
        3. Definition 7.3 (Message Channel)
        4. Definition 7.4 (Process)
        5. Definition 7.5 (Transition)
        6. Definition 7.6 (System State)
      3. Operational Model, Semantics Engine
      4. Interpreting PROMELA Models
      5. Three Examples
      6. Verification
      7. The Never Claim
    10. 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
    11. 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
    12. 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
    13. 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
    14. 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
    15. 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
    16. 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
    17. 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
    18. 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
    19. 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
    20. 18. Overview of SPIN Options
      1. Compile-Time Options
        1. -DCPP=..., -DSOLARIS, -D__FreeBSD__
        2. -DMAXQ=N
        3. -DNO_OPT
        4. -DNXT
        5. -DPC
        6. -DPRINTF
      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
    21. 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
        1. -DNOBOUNDCHECK
        2. -DNOFAIR
        3. -DSAFETY
      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
    22. Literature
    23. 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
    24. 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
    25. 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.
    26. D. Downloading Spin
      1. LTL Conversion
      2. Model Extraction
      3. Timeline Editor
    27. Tables and Figures
      1. Tables
      2. Figures