Especificación y desarrollo de software

Résumé

En esta tesis se presenta un modelo formal de sistema interactivo que, junto con un lenguaje basado en técnicas algebraicas, permite la especificación de las características relevantes de este tipo de sistemas, Se ha desarrollado el lenguaje Active GRALPLA con el que se pueden realizar especificaciones de sistemas interactivos a un nivel de abstracción alto. Junto con el lenguaje se han desarrollado un conjunto de herramientas que facilitan la construcción del software a partir de la especificación. Partiendo de técnicas basadas en métodos algebraicos se ha propuesto un modelo formal de sistema en base del concepto de objeto narrativo en el que se van a encapsular las características propias de la interacción (estado , representación gráfica, realimentación, ...). El modelo propuesto utiliza una representación del estado de cada uno de los objetos para un modelo de cálculo que permita obtener prototipos del sistema, en un lenguaje de alto nivel, partiendo de la especificación del mismo. El lenguaje y el modelo formal propuesto se han integrado dentro de un ciclo de vida de desarrollo de software basado en la utilización de prototipos para permitir la inclusión del usuario dentro de todo el proceso de desarrollo y que facilita el análisis de la usabilidad del sistema en las etapas iniciales del desarrollo. Se han propuesto una serie de ejemplos que ilustran el poder de expresividad del lenguaje. Y por último se han utilizado técnicas de verificación formal basadas en reescritura de términos para analizar la forma en la que se pueden probar propiedades propias de los sistemas interactivos como la alacanzabilidad, la visibilidad y la predecibilidad.