Model checking using Spin
Spin version 6.5.1
.
Introduction to model-checking using Spin
Spin models used in class:
Mod-4 counter
.
Traffic light
.
Traffic light, fixed version
.
LTL model-checking
.
Some
Lecture Notes
on Buchi automata and LTL model-checking.
Book
Chapter
by Madhavan Mukund on Finite-state Automata on Infinite Inputs, in Modern Applications of Automata Theory (World Scientific/IISc Press).