Observadores lineales: un lenguaje de especificación de propiedades para verificación de protocolos

• Autores: Pedro Merino Gómez
• Directores de la Tesis: José María Troya Linero (dir. tes.)
• Lectura: En la Universidad de Málaga ( España ) en 1998
• Idioma: español
• Tribunal Calificador de la Tesis: Carlos Delgado Kloos (presid.) , Ernesto Pimentel Sánchez (secret.) , Juan José Moreno Navarro (voc.) , Álvaro Suárez Sarmiento (voc.) , Arturo Azcorra Saloña (voc.)
• Texto completo no disponible (Saber más ...)
• Resumen

  • 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