Verificador de modelos SPIN

SPIN es una herramienta general para verificar la corrección de modelos de software concurrentes de forma rigurosa y mayormente automatizada. Fue desarrollada por Gerard J. Holzmann y otros miembros del grupo original de Unix del Centro de Investigación de Ciencias de la Computación de Bell Labs , a partir de 1980. El software está disponible gratuitamente desde 1991 y continúa evolucionando para adaptarse a los nuevos avances en el campo.

Los sistemas que se van a verificar se describen en Promela (Process Meta Language), que permite modelar algoritmos distribuidos asíncronos como autómatas no deterministas ( SPIN significa "Simple Promela Interpreter"). Las propiedades que se van a verificar se expresan como fórmulas de lógica temporal lineal (LTL) , que se niegan y luego se convierten en autómatas de Büchi como parte del algoritmo de verificación de modelos. Además de la verificación de modelos, SPIN también puede funcionar como simulador, siguiendo una posible ruta de ejecución a través del sistema y presentando el rastro de ejecución resultante al usuario.

A diferencia de muchos verificadores de modelos, SPIN no realiza la verificación de modelos por sí mismo, sino que genera código fuente en C para un verificador de modelos específico para cada problema. Esta técnica ahorra memoria y mejora el rendimiento, al tiempo que permite la inserción directa de fragmentos de código C en el modelo. SPIN también ofrece una gran cantidad de opciones para acelerar aún más el proceso de verificación de modelos y ahorrar memoria, tales como:

• reducción de orden parcial ;
• compresión de estado ;
• Hashing de estado de bits (en lugar de almacenar estados completos, solo se recuerda su código hash en un campo de bits; esto ahorra mucha memoria pero anula la completitud );
• Aplicación débil de la equidad.

Desde 1995, se han celebrado talleres SPIN (aproximadamente) anuales para usuarios de SPIN, investigadores y personas interesadas en general en la verificación de modelos .

En 2001, la Association for Computing Machinery otorgó a SPIN su premio System Software Award ^{[ 1 ] [ 2 ]} .

• NuSMV
• Comprobador de modelos Uppaal

• Holzmann, GJ, El verificador de modelos SPIN: Manual de introducción y referencia . Addison-Wesley , 2004. ISBN 0-321-22862-6.

• Sitio web de SPIN