Show simple item record

Especificación y verificación de sistemas reactivos utilizando métodos estructurados y lógica temporal

dc.contributor.advisorCorrales González, José Antonio 
dc.contributor.authorTuya González, Pablo Javier 
dc.contributor.otherIngeniería Eléctrica, Electrónica, de Computadores y Sistemas, Departamento de 
dc.date.accessioned2013-06-06T11:41:41Z
dc.date.available2013-06-06T11:41:41Z
dc.date.issued1995
dc.identifier.otherhttps://www.educacion.gob.es/teseo/mostrarRef.do?ref=146034
dc.identifier.urihttp://hdl.handle.net/10651/15766
dc.description.abstractEn 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.
dc.language.isospa
dc.titleEspecificación y verificación de sistemas reactivos utilizando métodos estructurados y lógica temporal
dc.typeinfo:eu-repo/semantics/doctoralThesis
dc.type.dcmitext
dc.local.notesTesis 1994-129


Files in this item

FilesSizeFormatView

There are no files associated with this item.

This item appears in the following Collection(s)

  • Tesis [6597]
    Tesis doctorales leídas en la Universidad de Oviedo

Show simple item record