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.
: 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/
- 13 Sep 2002