Grafo de Programa

Verificación y Validación de Software
Entrada 9

Para esta semana se nos pidió que modeláramos un sistema simple y lo representáramos mediante un sistema de transiciones o un grafo de programa, y opcionalmente crear la representación en PROMELA.

El sistema que modele para esta semana es muy simple. Se trata de la máquina donde se paga el pasaje en el Transmetro.

Descripción:
En el transporte "Transmetro" cuando un pasajero aborda el camión debe de ingresar la cantidad de $4.50 en la máquina. Una vez ingresada tal cantidad, se imprime un boleto con un código de barras. Esto se hace para evitar hacer doble pago al llegar a la estación, ya que con el mismo boleto del camión es posible subir al Metro.

Tomando en cuenta la máquina que recibe el dinero e imprime lo boletos, modele el sistema, que como podemos ver es muy simple, ya que solo consiste en una máquina que espera el ingreso de monedas, este esta contando el total, y cuando se tiene ya 4.50 en la máquina, se imprime un boleto. También hay que tomar en cuenta que no regresa cambio.

Por ser algo simple de entender, me pareció más práctico dibujar el sistema directo a un grafo de programa.

De la forma en que yo lo modele, supongo que desde que la máquina es encendida inicializa una variable para contar y otra que dice de cuanto fue la moneda. Hay un bucle al que entra inmediatamente después de esto, donde se espera a ingresar una moneda y se suma a la cantidad actual, y no se sale de ahí hasta que el total sean 4.50. Después de salir se imprime el boleto y se resta 4.50 al total, para regresar de nuevo al estado donde se espera el ingreso de monedas.

Es posible que el trabajo de esta máquina no sea secuencial sino que sea algo de forma paralelizada, por un lado la parte que toma las monedas, y por otro la que imprime el boleto. Esto se puede ver cuando un grupo de personas sube al camión, y solo una persona se encarga de depositar el dinero de todos en la máquina. La máquina no necesita que el usuario deje de meter monedas para poder imprimir los boletos, sino que cada que sobrepasa la cantidad de $4.50 imprime un boleto y resta la misma cantidad del total.

Entonces podemos verlo como dos tareas independientes de la siguiente forma.

Contador de monedas
Impresión del boleto

Representación PROMELA

PROMELA (Process/Protocol Meta Language) es un lenguaje de modelado de verificación. El lenguaje permite la creación dinámica de procesos concurrentes de un modelo, por ejemplo, los sistemas distribuidos. En modelos PROMELA, la comunicación a través de canales de mensajes puede ser definido para ser sincrónico o asincrónico. Un modelo escrito en PROMELA se puede analizar con el comprobador de modelos SPIN, para verificar que el sistema modelado produce el comportamiento deseado. [1]

Instalar SPIN en Ubuntu

1. Descargar la versión más reciente y compatible con tu sistema del ejecutable Spin. En mi caso he descargado el archivo spin622_linux64 para Linux.

Spin Precompiled Executables

2. De forma opcional es posible descargar un complemento gráfico para ejecutar y depurar el código. Aquí descargue el archivo ispin.tcl, que solo requiere de tener instalado el paquete tk8.4.

Spin Sources

3. Si no tienes instalado el paquete tk8.4, o no estas seguro de si ya lo tienes ejecuta el siguiente comando, si no esta instalado te pedirá tu aprobación para iniciar la instalación, en caso contrario te dirá que no es necesario instalar ningún paquete extra.

~$ sudo apt-get install tk8.4

4. Ahora vamos a la carpeta donde guardamos los archivos descargados y copiamos el ejecutable a la carpeta /usr/bin/ con el nombre de spin.

~$ cd Downloads/promela/
~$ sudo cp spin622_linux64 /usr/bin/spin

5. Para abrir la interfaz gráfica, estando en la carpeta donde tenemos guardado nuestro archivo ejecutamos la siguiente instrucción.

~$ wish ispin.tcl

6. Si quieres correr tus programas desde terminal solo es necesario ejecutar la siguiente instrucción, donde hello.pml es el nombre del archivo donde tienes tu código.

~$ spin -n2 hello.pml

Regresando al grafo de programa que mostré anteriormente, y basado en él, escribí un código sencillo de como debería trabajar este pequeño sistema, para luego probar desde interfaz gráfica. Para probar tome en cuenta que se ingresan siempre monedas de un peso y que la tarifa de la máquina es de 5 pesos.


Usando Spin desde interfaz gráfica es posible generar un diagrama desde el código escrito y su ejecución.

Ahora lo mismo, pero modelado como dos tareas independientes, incluyendo las líneas de skip, para uso de exclusión mutua, donde se accede a la variable "x".


Si corremos directo en terminal, podemos observar lo siguiente, que no es más que la ejecución de los dos procesos. Esto es solo una sección, ya que al correr el programa los procesos están en ejecución de forma infinita.

One coin introduced
One coin introduced
One coin introduced
One coin introduced
One coin introduced
    Ticket printed
One coin introduced
One coin introduced
One coin introduced
One coin introduced
One coin introduced
    Ticket printed

Podemos verificar el programa desde interfaz gráfica, y nos dará información acerca de nuestro programa. Nos da información acerca de cuantos estados y transiciones se crearon, si existe error alguno en la ejecución, la cantidad de memoria y procesos creados, etcétera.

Referencias:
[1] - Promela - Definición
Spin on Linux
Promela Model
Model Checking