EECI 2012: Computer Session: Spin: Difference between revisions
From Murray Wiki
Jump to navigationJump to search
No edit summary |
No edit summary |
||
| (8 intermediate revisions by one other user not shown) | |||
| Line 1: | Line 1: | ||
{{eeci-sp12 header|prev= | {{eeci-sp12 header|prev=Model Checking|next=Deductive Verification}} | ||
{{righttoc}} | {{righttoc}} | ||
| Line 5: | Line 5: | ||
== Lecture Materials == | == Lecture Materials == | ||
* [http://www.cds.caltech.edu/~murray/courses/ | * [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/C1_spin-15May12.pdf Lecture slides] | ||
* [http://www.cds.caltech.edu/~utopcu/ | * 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] | * [http://www.cds.caltech.edu/~utopcu/eeci2011/SPIN_cheat_sheet.pdf Sample SPIN commands] | ||
== Further Reading and Additional | == 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> | * <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. | |||
* | |||
Latest revision as of 14:49, 15 May 2012
| Prev: Model Checking | Course home | Next: Deductive Verification |
Hands-on model checking exercises using SPIN.
Lecture Materials
- Lecture slides
- Example promela files: lights_simple.pml, lights_distributed.pml, lights_synthesis.pml
- Sample SPIN commands
Further Reading
The SPIN Model Checker: Primer and Reference Manual, G. J. Holzmann, Addison-Wesley Professional, 2003. A comprehensive reference on Spin model checker
Additional Materials
- LTL2BA - a web page (and program) for converting LTL formulas to Buchi automata.
