You are here:
(27 Nov 2007,
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
ore topic actions
Topic revision: r3 - 27 Nov 2007,
Introduction to Software Technology
Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding UUCS?