Tesis doctoral de Tuya Gonzalez Pablo Javier
En esta tesis se integran los metodos estructurados (sa/rt) junto con metodos formales de verificacion basados en logica temporal. El objetivo es utilizar un metodo operacional (sa/rt) para especificar el comportamiento del sistema, y complementar esta con una especificacion declarativa basada en logica temporal (ctl). La consistencia entre una y otra son entonces verificadas utilizando un comprobador de modelos (smv). para poder analizar las propiedades del sistema se dota al metodo operacional de una sintaxis y semantica basadas en un sistema de transiciones, formando un modelo de procesos concurrentes entrelazados comunicados por variables compartidas. Ademas se enriquece la expresividad de los metodos sa/rt incorporando extensiones tales como la posibilidad de comunicacion entre procesos de forma sincrona y a traves de variables compartidas. Las transiciones pueden ser deterministas (con prioridades) o no deterministas. el modelo es traducido al lenguaje que sera utilizado por el comprobador de modelos smv. Se proporcionan los algoritmos de traduccion a este lenguaje. Con el objetivo de reducir el tamaño del modelo en el que se van a verificar las propiedades de seguridad, se proporciona un metodo para reducir su tamaño, y para componer especificaciones parciales. Tambien se tratan otras propiedades de vivacidad. finalmente, todo lo anterior se ilustra mediante tres ejemplos de diferentes tamaños, dos de ellos correspondientes a sistemas reales.
Datos académicos de la tesis doctoral «Especificacion y verificacion de sistemas reactivos utilizando metodos estructurados y logica temporal«
- Título de la tesis: Especificacion y verificacion de sistemas reactivos utilizando metodos estructurados y logica temporal
- Autor: Tuya Gonzalez Pablo Javier
- Universidad: Oviedo
- Fecha de lectura de la tesis: 01/01/1995
Dirección y tribunal
- Director de la tesis
- José Antonio Corrales Gonzalez
- Tribunal
- Presidente del tribunal: Pere Botella López
- Oliverio Gonzalez Alonso (vocal)
- Martinez Rodriguez Fco. Javier (vocal)
- Guillermo Ojea Merin (vocal)