English español
Search
 

Repositorio de la Universidad de Oviedo. > Producción Bibliográfica de UniOvi: RECOPILA > Tesis >

Please use this identifier to cite or link to this item: http://hdl.handle.net/10651/15766

Title: Especificación y verificación de sistemas reactivos utilizando métodos estructurados y lógica temporal
Author(s): Tuya González, Pablo Javier
Advisor: Corrales González, José Antonio
Other authors: Ingeniería Eléctrica, Electrónica, de Computadores y Sistemas, Departamento de
Issue date: 1995
Abstract: En esta tesis se integran los metodos estructurados (sa/rt) junto con métodos formales de verificación basados en lógica temporal. El objetivo es utilizar un método operacional (sa/rt) para especificar el comportamiento del sistema, y complementar esta con una especificación declarativa basada en lógica 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 método operacional de una sintaxis y semántica basadas en un sistema de transiciones, formando un modelo de procesos concurrentes entrelazados comunicados por variables compartidas. Además se enriquece la expresividad de los métodos sa/rt incorporando extensiones tales como la posibilidad de comunicación entre procesos de forma sincrona y a través de variables compartidas. Las transiciones pueden ser deterministas (con prioridades) o no deterministas. El modelo es traducido al lenguaje que será utilizado por el comprobador de modelos smv. Se proporcionan los algoritmos de traducción 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 método para reducir su tamaño, y para componer especificaciones parciales. También 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.
URI: http://hdl.handle.net/10651/15766
Identifier: https://www.educacion.gob.es/teseo/mostrarRef.do?ref=146034
Local notes: Tesis 1994-129
Appears in Collections:Tesis

Files in This Item:

There are no files associated with this item.



Exportar a Mendeley


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.

 

Base de Datos de Autoridades Biblioteca Universitaria Consultas / Sugerencias