Análisis de accesibilidad

El análisis de alcanzabilidad es una solución al problema de la alcanzabilidad en el contexto particular de los sistemas distribuidos. Se utiliza para determinar qué estados globales pueden ser alcanzados por un sistema distribuido compuesto por un cierto número de entidades locales que se comunican mediante el intercambio de mensajes.

El análisis de alcanzabilidad se introdujo en un artículo de 1978 para el análisis y la verificación de protocolos de comunicación . ^{[ 1 ]} Este artículo se inspiró en un artículo de Bartlett et al. de 1968 ^{[ 2 ]} que presentó el protocolo de bit alterno utilizando el modelado de estados finitos de las entidades del protocolo, y también señaló que un protocolo similar descrito anteriormente tenía un defecto de diseño. Este protocolo pertenece a la capa de enlace y, bajo ciertas suposiciones, proporciona como servicio la entrega correcta de datos sin pérdida ni duplicación, a pesar de la presencia ocasional de corrupción o pérdida de mensajes.

Para el análisis de accesibilidad, las entidades locales se modelan mediante sus estados y transiciones. Una entidad cambia de estado cuando envía un mensaje, consume un mensaje recibido o realiza una interacción en su interfaz de servicio local. El estado global${\displaystyle s=(s_{1},s_{2},...,s_{n},medium)}$ de un sistema con n entidades ^{[ 3 ]} está determinado por los estados${\displaystyle s_{i}}$ (i=1, ... n) de las entidades y el estado de la comunicación${\displaystyle medium}$En el caso más simple, el medio entre dos entidades se modela mediante dos colas FIFO en direcciones opuestas, que contienen los mensajes en tránsito (que se envían, pero aún no se consumen). El análisis de alcanzabilidad considera el comportamiento posible del sistema distribuido analizando todas las secuencias posibles de transiciones de estado de las entidades y los estados globales correspondientes alcanzados. ^{[ 4 ]}

El resultado del análisis de alcanzabilidad es un grafo de transición de estados global (también llamado grafo de alcanzabilidad) que muestra todos los estados globales del sistema distribuido que son alcanzables desde el estado global inicial, y todas las secuencias posibles de interacciones de envío, consumo y servicio realizadas por las entidades locales. Sin embargo, en muchos casos este grafo de transición no está acotado y no se puede explorar completamente. El grafo de transición se puede utilizar para comprobar fallos de diseño generales del protocolo (véase más adelante), pero también para verificar que las secuencias de interacciones de servicio de las entidades se corresponden con los requisitos dados por la especificación de servicio global del sistema. ^{[ 1 ]}

Acotación: El grafo de transición de estados global está acotado si el número de mensajes que pueden estar en tránsito está acotado y el número de estados de todas las entidades también lo está. La cuestión de si el número de mensajes permanece acotado en el caso de entidades con estados finitos no es, en general, decidible . ^{[ 5 ]} Normalmente, se trunca la exploración del grafo de transición cuando el número de mensajes en tránsito alcanza un umbral determinado.

Los siguientes son fallos de diseño:

• Bloqueo global: El sistema se encuentra en un bloqueo global si todas las entidades esperan a que se procese un mensaje y no hay ningún mensaje en tránsito. La ausencia de bloqueos globales se puede verificar comprobando que ningún estado en el grafo de alcanzabilidad sea un bloqueo global.
• Interbloqueos parciales: Una entidad se encuentra en estado de interbloqueo si espera el consumo de un mensaje y el sistema se encuentra en un estado global donde dicho mensaje no está en tránsito y nunca se enviará en ningún estado global al que se pueda acceder en el futuro. Esta propiedad no local se puede verificar mediante la comprobación del modelo en el grafo de alcanzabilidad.
• Recepción no especificada: Una entidad tiene recepción no especificada si el siguiente mensaje a consumir no se ajusta a la especificación de comportamiento de la entidad en su estado actual. La ausencia de esta condición se puede verificar comprobando todos los estados en el grafo de accesibilidad.

Como ejemplo, consideremos el sistema de dos entidades de protocolo que intercambian los mensajes ma , mb , mc y md entre sí, como se muestra en el primer diagrama. El protocolo se define por el comportamiento de las dos entidades, que se muestra en el segundo diagrama en forma de dos máquinas de estados. Aquí, el símbolo "!" significa enviar un mensaje, y "?" significa consumir un mensaje recibido. Los estados iniciales son los estados "1".

El tercer diagrama muestra el resultado del análisis de accesibilidad para este protocolo en forma de máquina de estados global. Cada estado global tiene cuatro componentes: el estado de la entidad de protocolo A (izquierda), el estado de la entidad B (derecha) y los mensajes en tránsito en el centro (parte superior: de A a B; parte inferior: de B a A). Cada transición de esta máquina de estados global corresponde a una transición de la entidad de protocolo A o de la entidad B. El estado inicial es [1, - - , 1] (sin mensajes en tránsito).

Se observa que este ejemplo tiene un espacio de estados global limitado: el número máximo de mensajes que pueden estar en tránsito simultáneamente es dos. Este protocolo presenta un bloqueo global, que corresponde al estado [2, - - , 3]. Si se elimina la transición de A en el estado 2 para consumir el mensaje mb , se producirá una recepción no especificada en los estados globales [2, ma mb ,3] y [2, - mb ,3].

El diseño de un protocolo debe adaptarse a las propiedades del medio de comunicación subyacente, a la posibilidad de que falle el interlocutor y al mecanismo que utiliza una entidad para seleccionar el siguiente mensaje. El medio de comunicación para los protocolos a nivel de enlace normalmente no es fiable y permite la recepción errónea y la pérdida de mensajes (modelada como una transición de estado del medio). Los protocolos que utilizan el servicio IP de Internet también deben contemplar la posibilidad de entrega fuera de orden. Los protocolos de nivel superior suelen utilizar un servicio de transporte orientado a sesiones, lo que significa que el medio proporciona una transmisión FIFO fiable de mensajes entre cualquier par de entidades. Sin embargo, en el análisis de algoritmos distribuidos , a menudo se tiene en cuenta la posibilidad de que alguna entidad falle por completo, lo que normalmente se detecta (como una pérdida de mensaje en el medio) mediante un mecanismo de tiempo de espera cuando no llega un mensaje esperado.

Se han formulado diferentes supuestos sobre si una entidad puede seleccionar un mensaje en particular para su consumo cuando han llegado varios mensajes y están listos para ser consumidos. Los modelos básicos son los siguientes:

• Cola de entrada única: Cada entidad dispone de una única cola FIFO donde se almacenan los mensajes entrantes hasta que se consumen. En este caso, la entidad no tiene poder de selección y debe consumir el primer mensaje de la cola.
• Múltiples colas: Cada entidad dispone de varias colas FIFO, una para cada interlocutor. En este caso, la entidad puede decidir, en función de su estado, de qué cola (o colas) debe consumir el siguiente mensaje de entrada.
• Grupo de recepción: Cada entidad dispone de un único grupo donde se almacenan los mensajes recibidos hasta que se consumen. En este grupo, la entidad puede decidir, según su estado, qué tipo de mensaje debe consumir a continuación (y esperar a recibir uno si aún no ha recibido ninguno), o bien consumir uno de un conjunto de tipos de mensajes (para gestionar las alternativas).

El artículo original que identificaba el problema de las recepciones no especificadas, ^{[ 6 ]} y gran parte del trabajo posterior, asumían una única cola de entrada. ^{[ 7 ]} A veces, las recepciones no especificadas se introducen por una condición de carrera , lo que significa que se reciben dos mensajes y su orden no está definido (lo cual suele ocurrir si provienen de diferentes socios). Muchos de estos fallos de diseño desaparecen cuando se utilizan múltiples colas o grupos de recepción. ^{[ 8 ]} Con el uso sistemático de grupos de recepción, el análisis de alcanzabilidad debería comprobar los interbloqueos parciales y los mensajes que permanecen indefinidamente en el grupo (sin ser consumidos por la entidad) ^{[ 9 ]}

La mayor parte del trabajo sobre modelado de protocolos utiliza máquinas de estados finitos (FSM) para modelar el comportamiento de las entidades distribuidas (véase también Máquinas de estados finitos comunicantes ). Sin embargo, este modelo no es lo suficientemente potente como para modelar parámetros de mensajes y variables locales. Por lo tanto, a menudo se utilizan los denominados modelos FSM extendidos, como los que admiten lenguajes como SDL o las máquinas de estados UML . Desafortunadamente, el análisis de alcanzabilidad se vuelve mucho más complejo para dichos modelos.

Un problema práctico del análisis de alcanzabilidad es la llamada "explosión del espacio de estados". Si las dos entidades de un protocolo tienen 100 estados cada una, y el medio puede incluir 10 tipos de mensajes, hasta dos en cada dirección, entonces el número de estados globales en el grafo de alcanzabilidad está limitado por el número 100 x 100 x (10 x 10) x (10 x 10), que es 100 millones. Por lo tanto, se han desarrollado varias herramientas para realizar automáticamente el análisis de alcanzabilidad y la verificación de modelos en el grafo de alcanzabilidad. Mencionamos solo dos ejemplos: el verificador de modelos SPIN y una caja de herramientas para la construcción y el análisis de procesos distribuidos .

• protocolos de comunicación
• Gerald Holzmann: Diseño y validación de protocolos informáticos , Prentice Hall , 1991.
• Gv Bochmann, D. Rayner y CH West: Algunas notas sobre la historia de la ingeniería de protocolos, Revista Computer Networks, 54 (2010), pp 3197–3209.