Introduction to Software Technology
WebHome
-
Education page
-
Course schedule
-
Assignments
-
Solutions
Master Program
Center
Center
Home
Courses
People
Projects
Page
Edit Page
Rename Page
Attach File
Printable
Wiki Source
More ...
Web
Recent Changes
Notify Service
News
Page Index
Search
More ...
Wiki
About TWiki
Text Formatting
Registration
Change Password
Reset Password
Users
Groups
Log In
or
Register
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