Spin Model Checker.
El SPIN model checker, puede verificar la correctitud de un sistema concurrente, para lo cual se necesita de un modelo que refeje los elementos esenciales del sistema. En caso de no satisfacer los requerimientos, se puede producir un ejemplo para demostrar el fallo. Hay dos formas de trabajar con