Soporte herramental para el Test Template Framework

Abstract

Este proyecto trata sobre la automatización y extensión del Test Template Framework (TTF). El TTF es un método de testing basado en modelos (MBT) especialmente orientado a testing de unidad a partir de especificaciones Z. Aunque el TTF es un método sólido y fue ampliamente estudiado desde su primera publicación, la comunidad de MBT fue perdiendo interés en él. Nosotros creemos que esto se debió, al menos en parte, a la falta o dificultad aparente en dotarlo de un apoyo herramental. De hecho, algunos han sugerido que la generación de casos de prueba abstractos siguiendo el TTF es una actividad manual que requiere que los usuarios manipulen predicados complejos. La intención de este proyecto es mostrar que estas conclusiones son al menos dudosas, implementando una herramienta, llamada Fastest. Fastest no solo es capaz de producir automáticamente casos de prueba abstractos sino que además podrá cubrir las necesidades de la comunidad Z en relación a herramientas de MBT.