Autor: LARRABEITI LOPEZ, David

Título: Contribución al análisis del espacio de estados de especificaciones LOTOS

Fecha: 1996

Materia: CIENCIAS TECNOLÓGICAS. Teseo;TECNOLOGÍA ENERGÉTICA. Teseo;TECNOLOGIA DE ORDENADORES. Teseo;DISEÑO DE SISTEMAS DE CÁLCULO. Teseo

Escuela: E.T.S. DE INGENIEROS DE TELECOMUNICACION

Departamento: INGENIERIA DE SISTEMAS TELEMATICOS

Acceso electrónico:

Director/a(s):

• Director/a: QUEMADA VIVES, Juan
• Director/a: PAVON GOMEZ, Santiago

Resumen: La primera fase en la mayoría de los algorítmos de validación y verificación de protocolos de comunicaciones existentes consiste en la generación del espacio de estados de una especificación formal del sistema. El principal obstáculo a la aplicación industrial de esta técnica es la elevada complejidad de los algorítmos de validación y el gran tamaño de los espacios de estados de los sistemas reales. La tesis aborda este problema en el ámbito del lenguaje LOTOS, con el desarrollo de una forma de representación y un método de exploración de estados compactos con diversas aplicaciones. El modelo propuesto permite una representación compacta del paralelismo, aliviando el problema de la explosión de estados derivados de la semántica de entrelazamiento de LOTOS. El algorítmo que transforma cualquier expresión LOTOS en una expresión equivalente en el nuevo cálculo se denomina expansión entrelazada. La expansión entrelazada genera una representación del sistema de transiciones donde los comportamientos entrelazantes son aislados, factorizados y conservados sin expandir. Esta representación supone una reducción de tamaño importante frente a la representación extensiva del sistema de transiciones, en aquellas especificaciones con un alto grado de entrelazamiento. Es por tanto adecuado para especificaciones escritas en estilo orientado a recursos donde el problema de la explosión de estados es mas frecuente e intenso. El desarrollo contiene la extensión del modelo a LOTOS completo y la comparación con algunos modelos con semánticas de concurrencia real relacionados, como las redes de Petri y las estructuras de eventos. Finalmente se estudia un mecanismo de exploración de estados que conserva la factorización de entrelazamiento y que es compatible con métodos de reducción basados en conjuntos de eventos persistentes. La implementación de la expansión entrelazada ha permitido contrastar empíricamente los resultados sobre especificaciones de complejidad media