EECI 2013: Computer Session: Spin

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

• SPIN web site

• LTL2BA - a web page (and program) for converting LTL formulas to Buchi automata.