Utilizando contratos de reuso con alloy

Abstract

El desarrollo de sistemas de software confiables exige la utilización de herramientas que posibiliten razonar rigurosamente acerca de su corrección y consistencia. Este tipo de análisis revela su importancia crítica cuando los sistemas evolucionan en el tiempo, sufriendo modificaciones que pueden alterar seriamente su eficacia o aún volverlos totalmente inútiles. El establecimiento del Proceso Unificado y el lenguaje UML como un estándar representan un avance, aunque insuficiente para alcanzar dichos objetivos. Más aún, el problema de la evolución ha recibido poco o ningún tratamiento en dicho contexto. En este trabajo se presenta una alternativa para avanzar en esa dirección, a través de la utilización de contratos de reuso[4] -expresados en UML- para describir evoluciones y su traducción a un lenguaje formal de primer orden, llamado Alloy[2], que provee herramientas para verificar algunas propiedades fundamentales de estos contratos. La traducción propuesta es sencilla, eficiente, modular, y provee bases ciertas para un proceso de evolución incremental de los diseños.