Tool Seminar:Lab Three

From Dependability

Overview | Schedule | Syllabus | 2006 Project Guidelines | Tool List | Editing Guidelines

 

 

We will be using SPIN model checker during Wednesday's lab.

The installation of SPIN will be a little complicated compared with the one-click installation of the tools we used in the last two labs. The installation of Xspin, the graphical interface of SPIN, will be even more complicated, and involves installation of other tools like tcl/tk, wish. So I decided to make my copy of SPIN available for all of you to use on the department's interactive Solaris servers (cobra, mamba, and adder). You can also choose to install your own copy of SPIN/Xspin. They have Unix/Windows/Mac versions. The downloading and installation instructions are here: http://spinroot.com/spin/Man/README.html.


Here are some instructions to use my installed version of SPIN/Xspin:

1. Log on to one of the interactice Solaris servers, e.g. cobra.

2. Make sure gcc is working correctly.

3. Assume you are using bash, enter: 

  export PATH=/uf21/xy9b/utils/bin:${PATH}

(You should enter this to change your environment whenever you login and want to use SPIN. Its effect will be undone when you log out.)

4. Enter: 

  spin -V

You should see something like: Spin Version 4.2.6 -- 27 October 2005.

Otherwise if you see: Spin Version 2.9.4 -- 4 November 1996, you haven't changed the environment correctly.

5. Assume you are using Windows, install Exceed from our department server: \\eirene\applications$\packages\exceed6.2UVaCS, and make sure it is runnable.

6. Assume you are using SecureCRT to connect to those Solaris servers, check the "Forward X11 Packets" option in session option or global option.

7. Start Exceed. (The shortcut should have the name "Exceed" in the start menu)

8. On the Solaris server (from SecureCRT), enter: 

  xspin

You should see the graphical interface pop up.

After step 1-4, you should be able to use the command line SPIN with no problem. Let me know whether you can or cannot go through step 5-8 to get Xspin running. If most of you cannot fire Xspin, I'll focus on the command line SPIN and just give a demo on Xspin.

Retrieved from "http://dependability.cs.virginia.edu/info/Tool_Seminar:Lab_Three"