EECI 2013: Computer Session: Spin: Difference between revisions
From Murray Wiki
Jump to navigationJump to search
(Created page with "{{eeci-sp13 header|prev=Model Checking|next=Deductive Verification}} {{righttoc}} Hands-on model checking exercises using SPIN. == Lecture Materials == * [http://www.cds.ca...") |
(No difference)
|
Latest revision as of 04:15, 11 March 2013
| 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.
