Análisis de accesibilidad

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

El análisis de accesibilidad se introdujo en un artículo de 1978 para el análisis y 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 bits alternos 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 alcanzabilidad, las entidades locales se modelan por 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 de un sistema con n entidades ^[3] está determinado por los estados (i=1, ... n) de las entidades y el estado de la comunicación . En el caso más simple, el medio entre dos entidades se modela por 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 posible comportamiento del sistema distribuido analizando todas las posibles secuencias de transiciones de estado de las entidades y los correspondientes estados globales alcanzados. ^[4]${\displaystyle s=(s_{1},s_{2},...,s_{n},medio)}$$estilo de visualización s_{i}}$${\displaystyle medio}$

El resultado del análisis de accesibilidad es un gráfico de transición de estado global (también llamado gráfico de accesibilidad) que muestra todos los estados globales del sistema distribuido que son accesibles desde el estado global inicial, y todas las posibles secuencias de interacciones de envío, consumo y servicio realizadas por las entidades locales. Sin embargo, en muchos casos este gráfico de transición no tiene límites y no se puede explorar por completo. El gráfico de transición se puede utilizar para verificar fallas generales de diseño del protocolo (ver más abajo), pero también para verificar que las secuencias de interacciones de servicio por parte de las entidades corresponden a los requisitos dados por la especificación de servicio global del sistema. ^[1]

Limitación: el gráfico de transición de estados global está limitado si el número de mensajes que pueden estar en tránsito está limitado y el número de estados de todas las entidades está limitado. La cuestión de si el número de mensajes permanece limitado en el caso de entidades de estados finitos en general no es decidible . ^[5] Por lo general, se trunca la exploración del gráfico de transición cuando el número de mensajes en tránsito alcanza un umbral determinado.

Los siguientes son defectos de diseño:

• Bloqueo global: el sistema se encuentra en un bloqueo global si todas las entidades esperan el consumo de 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 gráfico de accesibilidad sea un bloqueo global.
• Bloqueos parciales: una entidad se encuentra en un estado de bloqueo si espera el consumo de un mensaje y el sistema se encuentra en un estado global en el que 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 realizando una comprobación del modelo en el gráfico de accesibilidad.
• Recepción no especificada: una entidad tiene una recepción no especificada si el siguiente mensaje que se va a consumir no es el esperado por 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 gráfico de accesibilidad.

Como ejemplo, consideramos el sistema de dos entidades de protocolo que intercambian entre sí los mensajes ma , mb , mc y md , como se muestra en el primer diagrama. El protocolo se define por el comportamiento de las dos entidades, que se da 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 una 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 medio (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] (no hay mensajes en tránsito).

Se puede observar que este ejemplo tiene un espacio de estado global limitado: la cantidad máxima de mensajes que pueden estar en tránsito al mismo tiempo es dos. Este protocolo tiene un punto muerto global, que es el estado [2, - - , 3]. Si se elimina la transición de A en el estado 2 para consumir el mensaje mb , habrá 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 utilizado por una entidad para seleccionar el siguiente mensaje para su consumo. El medio de comunicación para 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 abordar la posibilidad de una entrega fuera de orden. Los protocolos de nivel superior normalmente utilizan 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 un mensaje esperado no llega.

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

• Cola de entrada única: Cada entidad tiene una única cola FIFO donde se almacenan los mensajes entrantes hasta que se consumen. Aquí la entidad no tiene poder de selección y debe consumir el primer mensaje de la cola.
• Colas múltiples: cada entidad tiene varias colas FIFO, una para cada interlocutor. Aquí la entidad tiene la posibilidad de decidir, en función de su estado, desde qué cola (o colas) debe consumirse el siguiente mensaje de entrada.
• Pool de recepción: Cada entidad dispone de un único pool donde se almacenan los mensajes recibidos hasta su consumo. Aquí la entidad tiene la potestad de decidir, en función de su estado, qué tipo de mensaje debe consumir a continuación (y esperar a recibir un mensaje si aún no ha recibido ninguno), o posiblemente consumir uno de un conjunto de tipos de mensajes (para poder gestionar alternativas).

El artículo original que identifica el problema de las recepciones no especificadas, ^[6] y gran parte del trabajo posterior, asumieron una única cola de entrada. ^[7] A veces, las recepciones no especificadas son introducidas por una condición de carrera , lo que significa que se reciben dos mensajes y su orden no está definido (lo que suele suceder 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 accesibilidad debería comprobar si hay bloqueos parciales y mensajes que permanecen para siempre 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 que se comunican ). 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 máquinas de estados UML . Desafortunadamente, el análisis de accesibilidad se vuelve mucho más complejo para dichos modelos.

Un problema práctico del análisis de la accesibilidad 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 gráfico de accesibilidad 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 accesibilidad y la verificación de modelos en el gráfico de accesibilidad. Mencionamos solo dos ejemplos: el verificador de modelos SPIN y una caja de herramientas para la construcción y 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, Computer Networks journal, 54 (2010), págs. 3197–3209.