Contribución al análisis del espacio de estados de especificaciones lotos

Abstract

La primera fase en la mayoria de los algoritmos de validacion y verificacion de protocolos de comunicaciones existentes consiste en la generacion del espacio de estados de una especificacion formal del sistema. El principal obstaculo a la aplicacion industrial de esta tecnica es la elevada complejidad de los algoritmos de validacion y el gran tamaño de los espacios de estados de los sistemas reales. La tesis aborda este problema en el ambito del lenguaje lotos, con el desarrollo de una forma de representacion y un metodo de exploracion de estados compactos con diversas aplicaciones. El modelo propuesto permite una representacion compacta del paralelismo, aliviando el problema de la explosion de estados derivados de la semantica de entrelazamiento de lotos. El algoritmo que transforma cualquier expresion lotos en una expresion equivalente en el nuevo calculo se denomina expansion entrelazada. La expansion entrelazada genera una representacion del sistema de transiciones donde los comportamientos entrelazantes son aislados, factorizados y conservados sin expandir. Esta representacion supone una reduccion de tamaño importante frente a la representacion 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 explosion de estados es mas frecuente e intenso. El desarrollo contiene la extension del modelo a lotos completo y la comparacion con algunos modelos con semanticas de concurrencia real relacionados, como las redes de petri y las estructuras de eventos. Finalmente se estudia un mecanismo de exploracion de estados que conserva la factorizacion de entrelazamiento y que es compatible con metodos de reduccion basados en conjuntos de eventos persistentes. La implementacion de la expansion entrelazada ha permitido contrastar empiricamente los resultados sobre especificacione