EECI 2012: Computer Session: Spin: Difference between revisions
From Murray Wiki
Jump to navigationJump to search
| Line 6: | Line 6: | ||
== Lecture Materials == | == Lecture Materials == | ||
* [http://www.cds.caltech.edu/~murray/courses/eeci-sp12/C1_spin-15May12.pdf Lecture slides] | * [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] | * 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/eeci2011/SPIN_cheat_sheet.pdf Sample SPIN commands] | * [http://www.cds.caltech.edu/~utopcu/eeci2011/SPIN_cheat_sheet.pdf Sample SPIN commands] | ||
Revision as of 13:40, 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,
- 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.
