EECI 2012: Computer Session: Spin: Difference between revisions
From Murray Wiki
Jump to navigationJump to search
| Line 10: | Line 10: | ||
== Further Reading == | == 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> | * <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 == | == Additional Materials == | ||
* [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. | ||
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.
