EECI 2012: Computer Session: Spin: Difference between revisions
From Murray Wiki
Jump to navigationJump to search
No edit summary |
|||
| 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/~utopcu/eeci-sp12/lights_simple.pml lights_simple.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 09:48, 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
- 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.
