Those Promela programs are executable by Spin. Spin is a commandline utility. To simplify the simulation and testing, it is recommended to use the Xspin GUI, at least for first-time users of Spin. Xspin is based on tcl/tk. Spin will compile Promela into a C program called pan.c, which is the translation of the Promela code to a Finite State Machine. This C program has to be compiled to run. So your machine must have a C compiler.
To run the Promela code included here on Windows, you will the following software. http://spinroot.com/spin/Man/README.html has a great guide on how to install Spin/Xspin on Unix, Windows, and Mac machines.
Following are the files related to my research.
| File | Type | Description | Link |
| zc-final.ppt | Presentation | My presentation on the final exam on 8/10/2006 | download |
| ccp.pml | Promela Code | Common Commitment Process is the generic model for commitment management | download |
| ccp_purchase_protocol.pml | Promela Code | The Promela model translated from OWL-P model for purchasing protocol | download |
| ccp-generic-cc.ltl | Protocol generic property claim | Check for property that the commitments will be in idle or discharged states. It needs to be adapted to the number of commitments structure allows in the model. | download |
| goods-pay.ltl | Protocol specific property claim | Check for property that when goods shipped, seller will receive the payment | download |
| pay-goods.ltl | Protocol specific property claim | Check for property that when buyer pays, it will eventually receive the goods. | download |
| reject-nopay.ltl | Protocol specific property claim | Check for property that when buyer rejects the seller's quote, it will not need to pay for anything | download |
| zcheng.zip | All sources | Promela and property files | download |