spin 3.5 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149
  1. .TH SPIN 1
  2. .SH NAME
  3. spin \- verification tool for concurrent systems
  4. .SH SYNOPSIS
  5. .B spin
  6. [
  7. .BI -n N
  8. ]
  9. [
  10. .B -cplgrsmv
  11. ]
  12. [
  13. .B -iat
  14. ]
  15. [
  16. .B -V
  17. ]
  18. [
  19. .I file
  20. ]
  21. .SH DESCRIPTION
  22. .I Spin
  23. is a tool for analyzing the logical consistency of
  24. concurrent systems, specifically communication protocols.
  25. The system is specified in a guarded command language called
  26. .SM PROMELA\c
  27. \&.
  28. The language, described in the references,
  29. allows for the dynamic creation of processes,
  30. nondeterministic case selection, loops, gotos,
  31. variables, and the specification of correctness requirements.
  32. The tool has fast algorithms for analyzing arbitrary
  33. liveness and safety conditions.
  34. .PP
  35. Given a model system specified in
  36. .SM PROMELA\c
  37. ,
  38. .I spin
  39. can perform interactive, guided, or random simulations
  40. of the system's execution
  41. or it can generate a C program that performs an exhaustive
  42. or approximate verification of the system.
  43. The verifier can check, for instance, if user specified system
  44. invariants are violated during a protocol's execution, or
  45. if non-progress execution cycles exist.
  46. .PP
  47. Without any options the program performs a random simulation of the system
  48. defined in the input
  49. .IR file ,
  50. default standard input.
  51. The option
  52. .BI -n N
  53. sets the random seed to the integer value
  54. .IR N .
  55. .PP
  56. The group of options
  57. .B -pglmrsv
  58. is used to set the level of information reported
  59. about the simulation run.
  60. Every line of output normally contains a reference to the source
  61. line in the specification that caused it.
  62. .TP
  63. .B c
  64. Show message send and receive operations in tabular form, but
  65. no other information about the execution.
  66. .TP
  67. .B p
  68. Show at each time step which process changed state and what source
  69. statement was executed.
  70. .TP
  71. .B l
  72. In combination with option
  73. .BR p ,
  74. show the current value of local variables of the process.
  75. .TP
  76. .B g
  77. Show the value of global variables at each time step.
  78. .TP
  79. .B r
  80. Show all message-receive events, giving
  81. the name and number of the receiving process
  82. and the corresponding source line number.
  83. For each message parameter, show
  84. the message type and the message channel number and name.
  85. .TP
  86. .B s
  87. Show all message-send events.
  88. .TP
  89. .B m
  90. Ordinarily, a send action will be delayed if the
  91. target message buffer if full.
  92. With this option a message sent to a full buffer is lost.
  93. The option can be combined with
  94. .B -a
  95. (see below).
  96. .TP
  97. .B v
  98. Verbose mode: add extra detail and include more warnings.
  99. .TP
  100. .BI i
  101. Perform an interactive simulation.
  102. .TP
  103. .B a
  104. Generate a protocol-specific verifier.
  105. The output is written into a set of C files, named
  106. .BR pan. [ cbhmt ],
  107. that can be compiled
  108. .RB ( "cc pan.c" )
  109. to produce an executable verifier.
  110. Systems that require more memory than available
  111. on the target machine can still be analyzed by compiling
  112. the verifier with a bit state space:
  113. .IP
  114. .B " cc -DBITSTATE pan.c
  115. .IP
  116. This collapses the state space to 1 bit per system state,
  117. with minimal side-effects.
  118. Partial order reduction rules normally take effect during the
  119. verification unless the compiler directive
  120. .B -DNOREDUCE
  121. is used.
  122. .IP
  123. The compiled verifiers have their own sets of options,
  124. which can be seen by running them with option
  125. .BR -? .
  126. .TP
  127. .B t
  128. If the verifier finds a violation of a correctness property,
  129. it writes an error trail.
  130. The trail can be inspected in detail by invoking
  131. .I spin
  132. with the
  133. .B -t
  134. option.
  135. In combination with the options
  136. .BR pglrsv ,
  137. different views of the error sequence are then be obtained.
  138. .TP
  139. .B V
  140. Print the version number and exit.
  141. .SH SEE ALSO
  142. G.J. Holzmann,
  143. .I
  144. Design and Validation of Computer Protocols,
  145. Prentice Hall, 1991.
  146. .br
  147. \(em, ``Using
  148. .SM SPIN\c
  149. \&''.