Lab 8 Assignment

In this lab, you will learn to use a tool for verifying UML Models. This tool is called SPIN.
  1. Within each project group, form two subgroups with 2 members each for this lab.
  2. Each subgroup must encode the state diagram of your project in PROMELA and type it in using your favorite text editor.
  3. Simulate your model in SPIN. Follow the directions below for using SPIN.
  4. Although this lab is not due till the beginning of next week, it will take some time to complete. Furthermore, next week's lab is dependent on this week's lab
  5. Next week, you will attempt to verify a couple of the critical properties that your project group came up with.
We will use XSpin, the graphical version of SPIN. To use XSpin:
  1. Go to start->programs->programming tools->spin->xspin
  2. Then open a promela file. Under "run", you'll find "syntax check" as well as "run simulation". For now, you'll just want to worry about simulation, not verification.
Relevant lecture notes covering Promela Language: Model Checking slides.

References

  1. Basic Spin Manual
  2. Concise Promela Reference

Promela Examples:
  Fall 99 Engine III waste sequence diagram
  Fall 99 Engine III class diagram
  Fall 99 Engine III shutdown sequence diagram
  Fall 99 Engine III timing diagram
  Fall 99 Engine III startup sequence diagram
  Fall 99 Engine III state diagram
  Fall 99 Engine III Example
  Home Heating System Example