Especificación, verificación y mantenimiento de requisitos funcionales con técnicas de descripción formal

Résumé

La tesis se enmarca dentro de la Ingenieria del Software, disciplina que tiene como objetivo proporcionar teorias, metodos y herramientas para el desarrollo de software de calidad, La aplicación de las metodologías de desarrollo software tradicionales a sistemas software complejos (sistemas software de comunicaciones) supuso un detrimento en la calidad de los productos software desarrollados, y un incremento en los costes de los mismos; debido, en gran medida, a la imposibilidad de probar el sistema hasta que se disponía de una implementación del mismo. Las tecnicas formales, basadas en la utilización de las matematicas como vehiculo para crear especificaciones de sistemas con una sintexis y semántica formalmente definida, permiten verificar y validar el sistema en todas las fases del proceso de desarrollo, reduciendo el riesgo de propagar errores a lo largo de dicho proceso. Sin embargo, y a pesar de las ventajas potenciales de los metodos formales, es escasa su integración en la industria del software. Este hecho esta motivado principalmente por: el desconocimiento (tanto de clientes como de diseñadores) de estas tecnicas; la inexistencia de herramientas apropiadas que permitan su aplicación practica; asi como su deficiente integración en el proceso de desarrollo software. En esta tesis se presenta un modelo de proceso de desarrollo software incremental totalmente formalizado. El trabajo se centra en las primeras etapas del proceso de desarrollo software (especificación, analisis y verificación de requisitos), abordando también la fase de diseño de la arquitectura del sistema y la fase de mantenimiento. El proceso incremental definido permite tratar cada refinamiento del sistema (incremento) de diferente forma, en función de la etapa de desarrollo en que se produzca. Esta idea se basa en dos aspectos fundamentales: por una parte, aprovechar las caracteristicas complementarias de los distintos tipos de tecnicas de des