Tesis doctoral de José Juan Pazos Arias
El trabajo de la tesis es una contribucion al diseño y desarrollo de sistemas con el lenguaje de especificacion formal lotos. 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 centro 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 unicamente los deseados. la logica temporal es un formalismo muy adecuado para la especificacion de las propiedades de un sistema. Dentro del trabajo de tesis, utilizamos la logica temporal para definir la semantica de programas lotos, obteniendo las siguientes ventajas: * verificacion de propiedades de programas lotos. Este tipo de verificacion ofrece una buen mecanismo de guia del proceso de diseño. * sintesis de programas lotos a partir de la propiedad que queremos que satisfaga. como resultado practico 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 verificacion y de sintesis comentadas.
Datos académicos de la tesis doctoral «Transformacion y verificacion con lotos«
- Título de la tesis: Transformacion y verificacion con lotos
- Autor: José Juan Pazos Arias
- Universidad: Politécnica de Madrid
- Fecha de lectura de la tesis: 01/01/1995
Dirección y tribunal
- Director de la tesis
- Carlos Delgado Kloos
- Tribunal
- Presidente del tribunal: Gonzalo León Serrano
- Angel Velazquez Iturbe (vocal)
- Pere Botella López (vocal)
- Santos Suarez José Manuel (vocal)