1
0

spin 6.5 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331
  1. .TH SPIN 1
  2. .SH NAME
  3. spin - verification tool for models of concurrent systems
  4. .SH SYNOPSIS
  5. .B spin
  6. .B -a
  7. [
  8. .B -m
  9. ]
  10. [
  11. .BI -P cpp
  12. ]
  13. .I file
  14. .PP
  15. .B spin
  16. [
  17. .B -bglmprsv
  18. ]
  19. [
  20. .BI -n N
  21. ]
  22. [
  23. .BI -P cpp
  24. ]
  25. .I file
  26. .PP
  27. .B spin
  28. .B -c
  29. [
  30. .B -t
  31. ]
  32. [
  33. .BI -P cpp
  34. ]
  35. .I file
  36. .PP
  37. .B spin
  38. .B -d
  39. [
  40. .BI -P cpp
  41. ]
  42. .I file
  43. .PP
  44. .B spin
  45. .B -f
  46. .I ltl
  47. .PP
  48. .B spin
  49. .B -F
  50. .I file
  51. .PP
  52. .B spin
  53. .B -i
  54. [
  55. .B -bglmprsv
  56. ]
  57. [
  58. .BI -n N
  59. ]
  60. [
  61. .BI -P cpp
  62. ]
  63. .I file
  64. .PP
  65. .B spin
  66. .B -M
  67. [
  68. .B -t
  69. ]
  70. [
  71. .BI -P cpp
  72. ]
  73. .I file
  74. .PP
  75. .B spin
  76. .BR -t [ \fIN ]
  77. [
  78. .B -bglmprsv
  79. ]
  80. [
  81. .BI -j N
  82. ]
  83. [
  84. .BI -P cpp
  85. ]
  86. .I file
  87. .PP
  88. .B spin
  89. .B -V
  90. .SH DESCRIPTION
  91. .I Spin
  92. is a tool for analyzing the logical consistency of
  93. asynchronous systems, specifically distributed software
  94. amd communication protocols.
  95. A verification model of the system is first specified
  96. in a guarded command language called
  97. .IR Promela .
  98. This specification language, described in the reference,
  99. allows for the modeling of dynamic creation of
  100. asynchronous processes,
  101. nondeterministic case selection, loops, gotos, local and
  102. global variables.
  103. It also allows for a concise specification of logical
  104. correctness requirements, including, but not restricted
  105. to requirements expressed in linear temporal logic.
  106. .PP
  107. Given a Promela model stored in
  108. .IR file ,
  109. .I spin
  110. can perform interactive, guided, or random simulations
  111. of the system's execution.
  112. It can also generate a C program that performs an exhaustive
  113. or approximate verification of the correctness requirements
  114. for the system.
  115. .
  116. .TP
  117. .B -a
  118. Generate a verifier (model checker) for the specification.
  119. The output is written into a set of C files, named
  120. .BR pan.[cbhmt] ,
  121. that can be compiled
  122. .RB ( "pcc pan.c" )
  123. to produce an executable verifier.
  124. The online
  125. .I spin
  126. manuals (see below) contain
  127. the details on compilation and use of the verifiers.
  128. .
  129. .TP
  130. .B -c
  131. Produce an ASCII approximation of a message sequence
  132. chart for a random or guided (when combined with
  133. .BR -t )
  134. simulation run. See also option
  135. .BR -M .
  136. .
  137. .TP
  138. .B -d
  139. Produce symbol table information for the model specified in
  140. .IR file .
  141. For each Promela object this information includes the type, name and
  142. number of elements (if declared as an array), the initial
  143. value (if a data object) or size (if a message channel), the
  144. scope (global or local), and whether the object is declared as
  145. a variable or as a parameter. For message channels, the data types
  146. of the message fields are listed.
  147. For structure variables, the third field defines the
  148. name of the structure declaration that contains the variable.
  149. .
  150. .TP
  151. .BI -f " ltl"
  152. Translate the LTL formula
  153. .I ltl
  154. into a
  155. .I never
  156. claim.
  157. .br
  158. This option reads a formula in LTL syntax from the second argument
  159. and translates it into Promela syntax (a
  160. .I never
  161. claim, which is Promela's
  162. equivalent of a Büchi Automaton).
  163. The LTL operators are written:
  164. .B []
  165. (always),
  166. .B <>
  167. (eventually),
  168. and
  169. .B U
  170. (strong until). There is no
  171. .B X
  172. (next) operator, to secure
  173. compatibility with the partial order reduction rules that are
  174. applied during the verification process.
  175. If the formula contains spaces, it should be quoted to form a
  176. single argument to the
  177. .I spin
  178. command.
  179. .
  180. .TP
  181. .BI -F " file"
  182. Translate the LTL formula stored in
  183. .I file
  184. into a
  185. .I never
  186. claim.
  187. .br
  188. This behaves identically to option
  189. .B -f
  190. but will read the formula from the
  191. .I file
  192. instead of from the command line.
  193. The file should contain the formula as the first line. Any text
  194. that follows this first line is ignored, so it can be used to
  195. store comments or annotation on the formula.
  196. (On some systems the quoting conventions of the shell complicate
  197. the use of option
  198. .BR -f .
  199. Option
  200. .B -F
  201. is meant to solve those problems.)
  202. .
  203. .TP
  204. .B -i
  205. Perform an interactive simulation, prompting the user at
  206. every execution step that requires a nondeterministic choice
  207. to be made. The simulation proceeds without user intervention
  208. when execution is deterministic.
  209. .
  210. .TP
  211. .B -M
  212. Produce a message sequence chart in Postscript form for a
  213. random simulation or a guided simulation
  214. (when combined with
  215. .BR -t ),
  216. for the model in
  217. .IR file ,
  218. and write the result into
  219. .IR file.ps .
  220. See also option
  221. .BR -c .
  222. .
  223. .TP
  224. .B -m
  225. Changes the semantics of send events.
  226. Ordinarily, a send action will be (blocked) if the
  227. target message buffer is full.
  228. With this option a message sent to a full buffer is lost.
  229. .
  230. .TP
  231. .BI -n N
  232. Set the seed for a random simulation to the integer value
  233. .IR N .
  234. There is no space between the
  235. .B -n
  236. and the integer
  237. .IR N .
  238. .
  239. .TP
  240. .B -t
  241. Perform a guided simulation, following the error trail that
  242. was produces by an earlier verification run, see the online manuals
  243. for the details on verification.
  244. .
  245. .TP
  246. .B -V
  247. Prints the
  248. .I spin
  249. version number and exits.
  250. .
  251. .PP
  252. With only a filename as an argument and no options,
  253. .I spin
  254. performs a random simulation of the model specified in
  255. the file (standard input is the default if the filename is omitted).
  256. If option
  257. .B -i
  258. is added, the simulation is
  259. .IR interactive ,
  260. or if option
  261. .B -t
  262. is added, the simulation is
  263. .IR guided .
  264. .PP
  265. The simulation normally does not generate output, except what is generated
  266. explicitly by the user within the model with
  267. .I printf
  268. statements, and some details about the final state that is
  269. reached after the simulation completes.
  270. The group of options
  271. .B -bglmprsv
  272. sets the desired level of information that the user wants
  273. about a random, guided, or interactive simulation run.
  274. Every line of output normally contains a reference to the source
  275. line in the specification that generated it.
  276. .
  277. .TP
  278. .B -b
  279. Suppress the execution of
  280. .I printf
  281. statements within the model.
  282. .TP
  283. .B -g
  284. Show at each time step the current value of global variables.
  285. .TP
  286. .B -l
  287. In combination with option
  288. .BR -p ,
  289. show the current value of local variables of the process.
  290. .TP
  291. .B -p
  292. Show at each simulation step which process changed state,
  293. and what source statement was executed.
  294. .TP
  295. .B -r
  296. Show all message-receive events, giving
  297. the name and number of the receiving process
  298. and the corresponding the source line number.
  299. For each message parameter, show
  300. the message type and the message channel number and name.
  301. .TP
  302. .B -s
  303. Show all message-send events.
  304. .TP
  305. .B -v
  306. Verbose mode, add some more detail, and generate more
  307. hints and warnings about the model.
  308. .SH SOURCE
  309. .B /sys/src/cmd/spin
  310. .SH SEE ALSO
  311. .in +4
  312. .ti -4
  313. .BR http://spinroot.com :
  314. .BR GettingStarted.pdf ,
  315. .BR Roadmap.pdf ,
  316. .BR Manual.pdf ,
  317. .BR WhatsNew.pdf ,
  318. .B Exercises.pdf
  319. .br
  320. .in -4
  321. G.J. Holzmann,
  322. .IR "Design and Validation of Computer Protocols" ,
  323. Prentice Hall, 1991.
  324. .br
  325. —, `Design and validation of protocols: a tutorial,'
  326. .IR "Computer Networks and ISDN Systems" ,
  327. Vol. 25, No. 9, 1993, pp. 981-1017.
  328. .br
  329. —, `The model checker Spin,'
  330. .IR "IEEE Trans. on SE" ,
  331. Vol, 23, No. 5, May 1997.