El proyecto Tokeneer es una iniciativa conjunta llevada adelante por la NSA (National Security Agency) y Praxis High Integrity Systems para desarrollar parte de un sistema seguro existente de acuerdo al proceso de desarrollo de “Corrección por Construcción” de Praxis. El objetivo es demostrar que desarrollar sistemas altamente seguros al nivel de rigor requerido por los niveles superiores de garantía del Criterio Común para la Evaluación de Seguridad en Tecnología Informática (Common Criteria) es posible. Toda la documentación del proyecto se encuentra disponible para permitir a la comunidad informática continuar la investigación en este tema. En particular, la especificación formal escrita en el lenguaje Z fue usada para esta tesina. El testing funcional basado en especificaciones permite una verificación formal y rigurosa de los sistemas de software. Con el propósito de facilitar la derivación automática de casos de prueba a partir de especificaciones en el lenguaje Z, Maximiliano Cristiá y Pablo Rodriguez Monetti desarrollaron la herramienta Fastest dentro del proyecto Flowx, financiado en conjunto por la empresa Flowgate Consulting y FONTAR (Fondo Tecnológico Argentino). El trabajo planteado en esta tesina consiste en la adaptación de la especificación de Tokeneer para poder generar casos de prueba con Fastest y comparar estos resultados con los obtenidos por Praxis. El estándar de LaTeX utilizado en la documentación de Tokeneer no se corresponde con el ISO aceptado por Fastest, por lo cual se modificaron las fuentes de la especificación para que sean compatibles con la herramienta de generación de casos de prueba. La versión de Fastest utilizada es un primer prototipo que aun no soporta toda la notación Z completa. La especificación de Tokeneer se adaptó también para que se adecúe a la porción de Z soportada por la herramienta. Se logró derivar el testing de unidad del sistema automáticamente demostrando que la herramienta puede ser utilizada en especificaciones de gran tamaño.