NuSMV

NuSMV

Desarrollador (es)	FBK-primero (Trento, Italia), CMU (Pittsburgh, PA), Universidad de Génova (Italia), Universidad de Trento (Italia)
Lanzamiento estable	2.6.0 / 14 de octubre de 2015 ; Hace 5 años ( 14 de octubre de 2015 )
Escrito en	ANSI C
Sistema operativo	Linux , Mac OS X , Microsoft Windows
Escribe	Comprobación del modelo
Licencia	LGPL v2.1
Sitio web	nusmv.fbk.eu

NuSMV es una reimplementación y extensión del verificador de modelos simbólicos SMV , la primera herramienta de verificación de modelos basada en diagramas de decisión binarios (BDD). ^[1] La herramienta ha sido diseñada como una arquitectura abierta para la verificación de modelos. Está dirigido a la verificación confiable de diseños de tamaño industrial, para su uso como backend para otras herramientas de verificación y como una herramienta de investigación para técnicas de verificación formales .

NuSMV se ha desarrollado como un proyecto conjunto entre el ITC-IRST ( Istituto Trentino di Cultura en Trento , Italia ), la Universidad Carnegie Mellon , la Universidad de Génova y la Universidad de Trento .

NuSMV 2 , versión 2 de NuSMV, hereda todas las funcionalidades de NuSMV. Además, combina la verificación de modelos basada en BDD con la verificación de modelos basada en SAT . ^[2] Es mantenido por Fondazione Bruno Kessler , la organización sucesora de ITC-IRST.

Funcionalidades

NuSMV admite el análisis de especificaciones expresadas en CTL y LTL . La interacción del usuario se realiza con una interfaz textual, así como en modo por lotes .

Ejecución de NuSMV de forma interactiva

El shell de interacción de NuSMV se activa desde el indicador del sistema de la siguiente manera:

[system_prompt] $ NuSMV -int NuSMV> ir a NuSMV>

NuSMV primero intenta leer y ejecutar comandos desde un archivo de inicialización si dicho archivo existe y es legible a menos que se pase -s en la línea de comandos. El archivo master.nusmvrc se busca en el directorio definido en la variable de entorno NUSMV _LIBRARY_PATH o en la ruta de biblioteca predeterminada si no se define dicha variable. Si no existe tal archivo, también se verificará el directorio de inicio del usuario y el directorio actual. Los comandos del archivo de inicialización se ejecutan consecutivamente. Cuando se completa la fase de inicialización, se muestra el shell NuSMV y el sistema ahora está listo para ejecutar los comandos del usuario.

Un comando NuSMV generalmente consta de un nombre de comando y argumentos para el comando invocado. Es posible hacer que NuSMV lea y ejecute una secuencia de comandos desde un archivo, a través de la opción de línea de comando -source :

[system_prompt] $ NuSMV -source cmd_file

Ejecución de lotes de NuSMV

Cuando no se especifica la opción -int, NuSMV se ejecuta como un programa por lotes, que tiene el siguiente formulario:

[system_prompt] $ NuSMV [ opciones de línea de comando ] input_file

Comprobación de la especificación LTL o CTL

NuSMV se puede utilizar para comprobar si las restricciones LTL o CTL predefinidas se cumplen para el modelo definido. Por ejemplo, tenemos una especificación CTL que queremos verificar:

CTLSPEC EF ( proc5 . Estado = crítico );   

Esta especificación verifica si existe una ruta de ejecución tal que el estado del proceso 5 sea crítico en algún momento. El usuario puede verificar si su modelo cumple con esta especificación usando los siguientes comandos.

[system_prompt] $ NuSMV [ comando opciones de línea ] archivo_entrada NuSMV> ir NuSMV> check_ctlspec

Si la especificación es verdadera, NuSMV le informará con

- la especificación EF proc5.state = crítica es verdadera > NuSMV

Sin embargo, si la especificación falla en algún estado, NuSMV devolverá un seguimiento completo de la ejecución que muestra cómo falla.

Ver también

• Spin Model Checker un verificador de modelos general para sistemas de software asíncronos
• CADP (Construcción y Análisis de Procesos Distribuidos), una caja de herramientas para el diseño formal de sistemas concurrentes asíncronos

Referencias

1. KL McMillan. Comprobación del modelo simbólico. En Kluwer Academic Publ., 1993.
2. A. Biere, A. Cimatti, E. Clarke e Y. Zhu. Comprobación de modelo simbólico sin BDD. En Herramientas y algoritmos para la construcción y análisis de sistemas, en TACAS'99, marzo de 1999.

enlaces externos

• Sitio web de NuSMV
• Sitio web de Nuseen : un conjunto de herramientas basadas en eclipse para el comprobador de modelos NuSMV.