SPIN

Ist

Spin is a state of the art automatic verifier. You describe your program in a language called PROMELA, which is especially suitable to describe concurrent programs. I will give a short demonstration, and we can do a small exercise to let you play a little bit with it.

  * *Exercise*: modify the 4-phases protocol so that it can also deal with damaged messages. To get you started, here is the Promela source of the 4-phases protocol: [[%ATTACHURL%/FourPhasesProtocol_v1.spin][FourPhasesProtocol_v1.spin]].

If you get stuck, here is a solution: [[%ATTACHURL%/FourPhasesProtocol_v3.spin][FourPhasesProtocol_v3.spin]]. Of course peeking into the solution will spoil the fun of puzzling it out yourself.

  * To start spin: do xspin from your xwindow shell.

  * Directory of spin in our system: /sw/pkg/spin

  * More info can be found in: /sw/pkg/spin/doc/HTML/index.html

  * Spin homepage [[http://cm.bell-labs.com/cm/cs/what/spin/]]


-- Main.WishnuPrasetya - 13 Sep 2002