NuXmv es una herramienta desarrollada por Fondazione Bruno Kessler como sucesor de otra herramienta anterior llamada nuSMV. NuSMV es software libre y también puede utilizarse para esta asignatura. Por el contrario, nuXmv se distribuye solamente en forma de binarios desde su página web, pero se puede usar gratuitamente para fines no comerciales o académicos.

Desde el punto de vista de la asignatura se puede usar indistintamente nuSMV o nuXmv. Ambas usan el mismo lenguaje de especificación.

• Manual de usuario
• Pequeño tutorial (L. Geatti)
• Curso de Patrick Trentin

Para ilustrar el uso de nuXmv vamos a implementar una máquina de estados como la que se muestra en la figura.

Figura: Control de luz en portal

El archivo de especificación SMV se descompone en varias secciones: variables de entrada (IVAR), variables de estado y de salida (VAR), asignaciones o transiciones de estados (ASSIGN), definición o asignación de nombres a expresiones comunes (DEFINE) y especificación de las propiedades formales (LTLSPEC y/o CTLSPEC).

main.smv
1MODULE main
2IVAR
3    button: boolean;
4
5VAR
6    timer: 0..20;
7    estado: {s0, s1};
8
9ASSIGN
10    init(estado):= s0;
11
12    next(estado) := case
13            estado = s0 & button : s1;
14            estado = s1 & timeout : s0;
15            TRUE: estado;
16        esac;
17
18    next(timer) := case
19            button : 20;
20            timeout: 0;
21            TRUE: timer - 1;
22        esac;
23
24DEFINE
25    lampara := estado = s1;
26    timeout := timer = 0;
27
28LTLSPEC G (button -> F lampara);
29LTLSPEC G (lampara & G !button -> F !lampara);

Hay otras formas de escribir lo mismo pero probablemente ésta es la más simple y menos propensa a error.

Para comprobar las propiedades podemos ejecutar:

1nuXmv> read_model -i main.smv
2nuXmv> go
3nuXmv> check_ltlspec

Durante el desarrollo puede ser útil explorar trazas de ejecución. Para simular una traza cualquiera podemos ejecutar las siguientes órdenes en nuXmv.

1nuXmv> pick_state -v
2nuXmv> simulate -k 50 -v

No esperamos que seas capaz de especificar las propiedades LTL y CTL de un sistema completo. No hace falta porque existe todo un catálogo de patrones de propiedades que pueden usarse para este fin. Determina las propiedades en términos coloquiales y busca las especificaciones que mejor se adaptan:

• Patrones de propiedades