Para efectuar el testing de Lisex se planea utilizar testing funcional a partir de especificaciones formales [HP95].

Lisex 0.0 no fue testado en profundidad como se debería hacer debido a la falta de recursos y a que el equipo de desarrollo espera poder automatizar gran parte de esta actividad fundamental. Hasta el momento sólo se generaron (manualmente) 365 casos de prueba a nivel del modelo y sólo se ejecutó el 10% de ellos sin que se haya encontrado algún error. Además, se cuenta con una versión preliminar de un algoritmo para extracción de conjuntos de prueba a partir de especificaciones Coq.

Testing funcional basado en especificaciones formales es una técnica de testing que utiliza una especificación formal de los requerimientos del sistema para generar los casos de prueba que más tarde se ejecutarán sobre el código. Además, permite utilizar el modelo formal como oráculo para determinar si el caso de prueba descubrió o no un error en el programa.

A grandes rasgos la técnica consta de las siguientes actividades:

1. Analizar sintácticamente la especificación tratando de revelar todas las alternativas funcionales que esta describe

   	El análisis anterior genera como resultado una familia de conjuntos de prueba cada uno de los cuales representa una alternativa funcional diferente
   	En el análisis se aplica una estrategia de testing (por ejemplo, forma normal disyuntiva, mutación de especificaciones, propagación de sub-dominios, etc.)

2. Se aplica otra estrategia de testing a los conjuntos de prueba generados en el primer análisis generando una nueva familia de conjuntos de prueba (no menos poblada que la anterior)
3. El proceso anterior se repite iterativamente hasta que se alcance la cantidad de conjuntos de prueba requerida
4. De cada conjunto de prueba de la última familia generada se elige un representante
5. Cada representante se proyecta a nivel de la implementación
6. Los casos de prueba así obtenidos se ejecutan sobre el código
7. Se captura la salida de cada ejecución
8. Se proyecta a nivel del modelo cada salida
9. Cada par (caso de prueba, salida) se aplica a la especificación como forma de comprobar que la salida es la esperada (por la especificación para esa entrada)
10. Si la especificación indica que una salida no es la que corresponde a la entrada, se ha descubierto un error

El proceso continúa corrigiendo el código y volviendo a ejecutar todos los casos que sea necesario.

El equipo Lisex ha documentado los casos de prueba a nivel del modelo en formato HTML y Postscript.