**This is an old revision of the document!**


Objectives:

  • Download and install SPIN
  • Run a few simple examples with SPIN

Problems

  1. (5 points) Download and install the SPIN model checker. See the Tools page for some suggestions. Submit a screen shot from the command spin -?
  2. (20 points) Write a PROMELA model that starts no more than N processes randomly where N is given with a #define. Here the init process is not part of N. Write a process to start that behaves as described in each of the below variations. Run each one of the models in both simulation and verification mode. Report the number of states found for N = 5 in verification mode for each one. Put that in a comment block in the model.
    • the N processes output their process ID in the order of creation.
    • the N processes output their process ID in the reverse order of creation.
    • the N processes actually exit in the reverse order of creation.
    • Try N processes actually exit in the actual order of creation. Explain what happens in this variant of the model?
cs-486/homework-0.1578786955.txt.gz · Last modified: 2020/01/11 16:55 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0