EECI 2012: Computer Session: Spin: Difference between revisions
From Murray Wiki
Jump to navigationJump to search
No edit summary |
|||
| (4 intermediate revisions by one other user not shown) | |||
| 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] | ||
| Line 13: | Line 13: | ||
== Additional Materials == | == 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. | * [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.
