Lo más rápido

Fastest es una herramienta de prueba basada en modelos que trabaja con especificaciones escritas en la notación Z. La herramienta implementa ^{[ 1 ]} el marco de plantillas de prueba (TTF) propuesto por Phil Stocks y David Carrington. ^{[ 2 ]}

Fastest presenta una interfaz de usuario de línea de comandos. El usuario primero debe cargar una especificación Z escrita en formato LaTeX que verifique el estándar ISO . ^{[ 3 ]} Luego, el usuario debe ingresar una lista de las operaciones a probar, así como las tácticas de prueba que se aplicarán a cada una de ellas. En un tercer paso, Fastest genera el árbol de pruebas de cada operación. Una vez generados los árboles de pruebas, los usuarios pueden explorarlos, así como 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 podados los árboles de pruebas, los usuarios pueden indicarle a Fastest que encuentre un caso de prueba abstracto para cada hoja en cada árbol de pruebas. ^{[ 4 ]}

Actualmente, Fastest admite las siguientes tácticas de prueba:

• Forma Normal Disyuntiva (FND). Es la única táctica de prueba que se aplica por defecto (independientemente de si el usuario ha añadido o no otras tácticas de prueba) y la primera que se aplica.
• Particiones estándar (SP). El usuario puede agregar, modificar y eliminar particiones estándar para cualquier operador matemático Z predefinido simplemente editando un archivo de texto . ^{[ 5 ]}
• Tipos Libres (FT)
• En la extensión de conjuntos (ISE)
• Subconjunto propio de extensión de conjunto (PSSE)
• Subconjunto de extensión de conjunto (SSE)

Fastest proporciona dos formas de podar los árboles de prueba: ^{[ 6 ]}

• Poda automática.

Para podar un árbol de pruebas, Fastest analiza el predicado de cada hoja para determinar si es una contradicción o no. Dado que este problema es indecidible , la herramienta implementa un algoritmo de mejor esfuerzo que los usuarios pueden mejorar. El aspecto más importante del algoritmo es una biblioteca de teoremas de eliminación, cada uno de los cuales representa una familia de contradicciones. Esta biblioteca puede ser ampliada por los usuarios simplemente editando un archivo de texto. Los teoremas de eliminación son conjunciones de predicados atómicos Z paramétricos.

• Poda manual.

Los usuarios más rápidos pueden podar subárboles o hojas individuales de árboles de prueba mediante dos comandos. Estos comandos podarán todas las clases de prueba en el subárbol, estén vacías o no. El objetivo principal de estos comandos es permitir a los ingenieros reducir el número de casos de prueba o eliminar los que no sean importantes.

La herramienta encuentra casos de prueba abstractos calculando un modelo finito para cada hoja en un árbol de prueba. ^{[ 7 ]} 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 de 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 es insatisfacible o el modelo finito es inadecuado). En este último caso, el usuario tiene la oportunidad de ayudar a la herramienta a encontrar el modelo finito correcto o de podar la clase de prueba porque es insatisfacible.

Fastest es una aplicación Java basada en el proyecto Community Z Tools (CZT) . La herramienta se puede utilizar en uno de dos modos: ^{[ 8 ]}

• En modo distribuido, Fastest funciona como una aplicación cliente-servidor . La aplicación puede instalarse en varios ordenadores, cada uno de los cuales actúa como cliente, servidor o ambos. Los usuarios acceden a la aplicación a través de clientes que envían clases de prueba a servidores (denominados servidores de prueba ) que intentan encontrar un caso de prueba abstracto a partir de ellas. De esta forma, la tarea más pesada se distribuye entre el mayor número posible de ordenadores. Dado que el cálculo de un caso de prueba abstracto a partir de una clase de prueba es completamente independiente, esta arquitectura acelera todo el proceso proporcionalmente al número de servidores de prueba.
• En el modo de aplicación, cada instancia de Fastest es completamente independiente de las demás. Todas las tareas se calculan en el ordenador local.

paquete client.blogic.testing.ttree.tactics ;import java.util.* ; import net.sourceforge.czt.z.ast.Spec ; import common.z.TClass ; import common.z.OpScheme ;/** * Interfaz que abstrae una táctica de prueba (necesaria para generar árboles de prueba) y * hace posible su aplicación a una clase de prueba para generar otras nuevas. */ public interface Tactic { /**  * Aplica esta táctica a la clase de prueba especificada y devuelve la lista con  * las clases de prueba generadas.  * @param tClass  * @return  */ public List < TClass > applyTactic ( TClass tClass ); /**  * Establece la especificación del sistema bajo prueba.  * @param opScheme  */ public void setSpec ( Spec spec ); /**  * Obtiene el cuadro de esquema Z de la operación bajo prueba.  * @return  */ public Spec getSpec (); /**  * Establece el cuadro de esquema Z de la operación bajo prueba.  * @param opScheme  */ public void setOriginalOp ( OpScheme opScheme ); /**  * Obtiene el cuadro de esquema Z de la operación bajo prueba.  * @return  */ public OpScheme getOriginalOp (); /**  * Analiza los parámetros de esta táctica.  * @param str  * @return  */ public boolean parseArgs ( String str ); /**  * Establece la instancia de TacticInfo asociada a este objeto.  * @param tacticInfo  */ public void setTacticInfo ( TacticInfo tacticInfo ); /**  * Obtiene la instancia de TacticInfo asociada a este objeto.  * @return  */ public TacticInfo getTacticInfo (); /**  * Obtiene la descripción de esta táctica.  * @return la cadena con la descripción de esta táctica.  */ public String getDescription (); /**  * Establece la descripción de esta táctica.  * @param description  */ public void setDescription ( String description ); }

• Marco de plantillas de prueba
• Pruebas basadas en modelos

• Cristiá, Maximiliano; Rodríguez Monetti, Pablo (2009). "Implementación y aplicación del marco Stocks-Carrington para pruebas basadas en modelos". Métodos formales e ingeniería de software, 11.ª Conferencia Internacional sobre Métodos de Ingeniería Formal, ICFEM 2009. Río de Janeiro, Brasil: Springer-Verlag .
• Stocks, Phil; Carrington, David (1996), "Un marco para pruebas basadas en especificaciones", IEEE Transactions on Software Engineering , 22 (11): 777–793 , doi : 10.1109/32.553698.
• Tecnología de la Información — Notación de Especificación Formal Z — Sintaxis, Sistema de Tipos y Semántica (PDF de 1 MB) , 2002, 196 páginasISO /IEC 13568:2002
• Cristiá, Maximiliano; Albertengo, Pablo; Rodríguez Monetti, Pablo (2010). "Poda de árboles de prueba en el marco de plantillas de prueba mediante la detección de contradicciones matemáticas". 8.ª Conferencia Internacional IEEE sobre Ingeniería de Software y Métodos Formales (SEFM), 2010. Pisa, Italia: IEEE .