Fastest es una herramienta de prueba basada en modelos que funciona con especificaciones escritas en notación Z. La herramienta implementa ( Cristia y Rodríguez Monetti 2009 ) el Marco de plantilla de prueba (TTF) propuesto por Phil Stocks y David Carrington en ( Stocks y Carrington 1996 ).
Fastest presenta una interfaz de usuario de línea de comandos. El usuario primero necesita cargar una especificación Z escrita en formato LaTeX verificando el estándar ISO ( Estándar Z 2002 ). Luego, el usuario debe ingresar una lista de las operaciones a probar, así como las tácticas de prueba para aplicar a cada una de ellas. En un tercer paso Fastest genera el árbol de pruebas de cada operación. Una vez que se han generado los árboles de prueba, los usuarios pueden examinarlos y sus clases de prueba y, lo que es más importante, pueden podar cualquier clase de prueba de forma automática o manual . Una vez que se han podado los árboles de prueba, los usuarios pueden indicar a Fastest que encuentre un caso de prueba abstractopara cada hoja en cada árbol de prueba. ( Cristia, Rodríguez Monetti y Albertengo 2009 )
La herramienta encuentra casos de prueba abstractos calculando un modelo finito para cada hoja en un árbol de prueba ( Cristia y Rodríguez Monetti 2009 ). Los modelos finitos se calculan restringiendo el tipo de cada variable VIS a un conjunto finito y luego calculando el producto cartesiano entre estos conjuntos. Cada predicado hoja se evalúa en cada elemento de este producto cartesiano hasta que uno satisface el predicado (lo que significa que se encontró un caso de prueba abstracto) o hasta que se agota (lo que significa que la clase de prueba no es satisfactoria o el modelo finito es inadecuado). En el último caso, el usuario tiene la oportunidad de ayudar a la herramienta a encontrar el modelo finito correcto o de eliminar la clase de prueba porque no es satisfactoria.
Fastest es una aplicación Java basada en el proyecto Community Z Tools (CZT) . La herramienta se puede utilizar en uno de dos modos ( Cristia y Rodríguez Monetti 2009 ):
Como puede verse en la presentación TTF , las tácticas de prueba son esenciales para el método. Son las herramientas que los ingenieros deben utilizar para crear los casos de prueba más interesantes posibles. Entonces, cuantas más tácticas de prueba sólidas estén disponibles para los ingenieros, mejor.
En Fastest, los usuarios pueden agregar sus propias tácticas de prueba implementando la interfaz Tactic proporcionada por la herramienta. Esta interfaz tiene métodos para configurar y aplicar tácticas de prueba. La definición de interfaz es la siguiente: