https://murray.cds.caltech.edu/index.php?action=history&feed=atom&title=EECI_2013%3A_Computer_Session%3A_Spin 2026-07-27T08:51:53Z Revision history for this page on the wiki MediaWiki 1.44.2 https://murray.cds.caltech.edu/index.php?title=EECI_2013:_Computer_Session:_Spin&diff=15596&oldid=prev 2013-03-11T04:15:07Z

<p>Created page with &quot;{{eeci-sp13 header|prev=Model Checking|next=Deductive Verification}} {{righttoc}} Hands-on model checking exercises using SPIN. == Lecture Materials == * [http://www.cds.ca...&quot;</p> <p><b>New page</b></p><div>{{eeci-sp13 header|prev=Model Checking|next=Deductive Verification}}<br /> <br /> {{righttoc}}<br /> Hands-on model checking exercises using SPIN.<br /> <br /> == Lecture Materials ==<br /> * [http://www.cds.caltech.edu/~murray/courses/eeci-sp13/C1_spin-19Mar13.pdf Lecture slides]<br /> * Example promela files: [http://www.cds.caltech.edu/~murray/courses/eeci-sp13/lights_simple.pml lights_simple.pml], [http://www.cds.caltech.edu/~murray/courses/eeci-sp13/lights_distributed.pml lights_distributed.pml], [http://www.cds.caltech.edu/~murray/courses/eeci-sp13/lights_synthesis.pml lights_synthesis.pml]<br /> * [http://www.cds.caltech.edu/~utopcu/eeci2011/SPIN_cheat_sheet.pdf Sample SPIN commands]<br /> <br /> == Further Reading ==<br /> * &lt;p&gt;[http://www.amazon.com/SPIN-Model-Checker-Primer-Reference/dp/0321228626/ref=sr_1_1?ie=UTF8&amp;qid=1297068669&amp;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 &lt;/p&gt;<br /> <br /> == Additional Materials ==<br /> * &lt;p&gt;[http://spinroot.com/spin/whatispin.html SPIN web site] &lt;/p&gt;<br /> * [http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ LTL2BA] - a web page (and program) for converting LTL formulas to Buchi automata.</div>

Murray