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éetodo de testing basado en modelos (MBT) especialmente orientado a testing de unidad a partir de especifi caciones Z. Aunque el TTF es un m etodo s ólido y fue ampliamente estudiado desde su primera publicaci ón, la comunidad de MBT fue perdiendo inter és en el. Nosotros creemos que esto se debi o, al menos en parte, a la falta o di cultad 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 aticamente casos de prueba abstractos sino que además podrá cubrir las necesidades de la comunidad Z en relaci ón a herramientas de MBT.