EECI 2012: Computer Session: Spin: Difference between revisions
From Murray Wiki
Jump to navigationJump to search
No edit summary |
|||
| Line 9: | Line 9: | ||
* [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 | == Further Reading == | ||
* <p>[http://spinroot.com/spin/whatispin.html SPIN web site] </p> | * <p>[http://spinroot.com/spin/whatispin.html SPIN web site] </p> | ||
* <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> | * <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 == | |||
* [http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ LTL2BA] - a web page (and program) for converting LTL formulas to Buchi automata. | |||
Revision as of 09:51, 14 May 2012
| Prev: Model Checking | Course home | Next: Deductive Verification |
Hands-on model checking exercises using SPIN.
Lecture Materials
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.
