Especificación y desarrollo de software

• Autores: Francisco Luis Gutiérrez Vela
• Directores de la Tesis: Juan Carlos Torres Cantero (dir. tes.) , Francisco Miguel Gea Megías (dir. tes.)
• Lectura: En la Universidad de Granada ( España ) en 2002
• Idioma: español
• Tribunal Calificador de la Tesis: Roberto Moriyón Salomón (presid.) , José Parets Llorca (secret.) , Jesús Lorés Vidal (voc.) , Julio Abascal González (voc.) , María José Rodríguez Fortiz (voc.)
• Texto completo no disponible (Saber más ...)
• Resumen

  • 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.