View source for EECI 2012: Computer Session: Spin

{{eeci-sp12 header|prev=Model Checking|next=Deductive Verification}}

{{righttoc}}
Hands-on model checking exercises using SPIN.

==  Lecture Materials ==
* [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/C1_spin-15May12.pdf Lecture slides]
* Example promela files: [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/lights_simple.pml lights_simple.pml], [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/lights_distributed.pml lights_distributed.pml], [http://www.cds.caltech.edu/~utopcu/EECI2012/lights_synthesis.pml lights_synthesis.pml]
* [http://www.cds.caltech.edu/~utopcu/eeci2011/SPIN_cheat_sheet.pdf Sample SPIN commands]

== Further Reading ==
* <p>[http://www.amazon.com/SPIN-Model-Checker-Primer-Reference/dp/0321228626/ref=sr_1_1?ie=UTF8&qid=1297068669&sr=8-1 The SPIN Model Checker: Primer and Reference Manual], G. J. Holzmann, Addison-Wesley Professional, 2003. A comprehensive reference on Spin model checker </p>

== Additional Materials ==
* <p>[http://spinroot.com/spin/whatispin.html SPIN web site] </p>
* [http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ LTL2BA] - a web page (and program) for converting LTL formulas to Buchi automata.