Tesis doctoral de Pedro Merino Gomez
La verificación de protocolos es una actividad fundamental para localizar errores de diseño y para garantizar que un sistema distribuido tenga el funcionamiento deseado. La automatización de esta tarea supone comparar una especificación del comportamiento esperado frente a otra especificación que se propone como un diseño para el sistema. Aunque la verificación automática es una técnica relativamente reciente, existe ya una gran variedad de lenguajes para la descripción de estos dos componentes, así como diversos criterios para decidir si el diseño satisface la especificación. En este trabajo se propone un nuevo lenguaje para describir el funcionamiento deseado de los protocolos. este lenguaje de especificación de propiedades, que se denomina observadores lineales, puede considerarse como una versión ejecutable de un fragmento de lógica lineal. El nuevo formalismo permite especificar propiedades en las que es importante el número de veces que ocurren los eventos, como pueden ser las propiedades que incluyen parámetros de calidad de servicio (cds), estrategias de planificación o números de secuencia. Además, el lenguaje incorpora mecanismos para especificar y analizar sistemas con configuraciones dinámicas. su base lógica facilita tanto su uso en un marco de programación declarativa, como la aplicación de técnicas propias de la lógica lineal para el análisis y la transformación de la propia especificación de la propiedad. el algoritmo de verificación propuesto consiste en realizar el análisis al mismo tiempo que se genera el espacio de estados del protocolo, e incluye métodos de optimización existentes para reducir las necesidades de memoria y tiempo. Como novedad se presenta un método de poda del árbol de estados, que se basa en técnicas de programación entera para determinar si es posible o no satisfacer la propiedad en función del análisis ya realizado. para demostrar la utilidad p
Datos académicos de la tesis doctoral «Observadores lineales: un lenguaje de especificacion de propiedades para verificacion de protocolos.«
- Título de la tesis: Observadores lineales: un lenguaje de especificacion de propiedades para verificacion de protocolos.
- Autor: Pedro Merino Gomez
- Universidad: Málaga
- Fecha de lectura de la tesis: 11/09/1998
Dirección y tribunal
- Director de la tesis
- José María Troya Linero
- Tribunal
- Presidente del tribunal: Carlos Delgado kloos
- Álvaro Suarez sarmiento (vocal)
- Juan José Moreno navarro (vocal)
- arturo Azkorra saloña (vocal)