Tesis Doctorales UPM: Consulta online

Resumen: El trabajo de la tesis es una contribución al diseño y desarrollo de sistemas con el lenguaje de especificación formal LOTOS. El lenguaje LOTOS facilita el diseño de sistemas mediante refinamientos sucesivos: el sistema se construye de forma incremental como una secuencia de pasos dirigida a obtener un producto final que satisfaga los requisitos expresados inicialmente por el usuario o cliente. El objetivo del trabajo de tesis se centró en el diseño de una herramienta que diera soporte a este proceso de diseño, es decir, automatizara todas las tareas rutinarias. En este proceso de diseño es conveniente disponer de un mecanismo que permita asegurar que los efectos de un refinamiento son únicamente los deseados. La lógica temporal es un formalismo muy adecuado para la especificación de las propiedades de un sistema. Dentro del trabajo de tesis, utilizamos la lógica temporal para definir la semántica de programas LOTOS, obteniendo las siguientes ventajas: 1.- Verificación de propiedades de programas LOTOS. Este tipo de verificación ofrece un buen mecanismo de guía del proceso de diseño. 2.- Síntesis de programas LOTOS a partir de la propiedad que queremos que satisfaga. Como resultado práctico del trabajo realizado, se ha desarrollado un entorno que da soporte al desarrollo por refinamientos sucesivos de un sistema con LOTOS y que ofrece de forma integrada las facilidades de verificación y de síntesis comentadas