Las Metodologías Ágiles (MA) son ampliamente elegidas en proyectos de software actuales. No obstante, frecuentemente deben afrontar problemas inherentes a su falta de formalidad; tales como la dificultad de recoger, entender y mantener los requerimientos del sistema.
Alloy es un lenguaje formal, soportado por una amigable herramienta de verificación y validación. Estas caracterísiticas pueden ser aprovechadas en favor de las MA. La línea de investigación se enfoca puntualmente en la adopción de Alloy dentro de las MA mas populares. Esto incluye analizar no solo los beneficios, sino también la forma en que dicho lenguaje puede ser incorporado en el proceso de desarrollo de software.