SPIN

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: FourPhasesProtocol_v1.spin.

If you get stuck, here is a solution: 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/

-- WishnuPrasetya - 13 Sep 2002