VERIFICACIÓN DE LOS PROTOCOLOS

VERIFICACIÓN DE LOS PROTOCOLOS

Se requiere mucha investigación para encontrar técnicas matemáticas formales con las cuales especificar y verificar los protocolos. En las siguientes secciones veremos algunos modelos y técnicas.

MODELOS DE MÁQUINAS DE ESTADO FINITO

Con esta técnica, cada máquina de protocolo (es decir, emisor o receptor) siempre está en un estado específico en cualquier instante. Su estado consiste en todos los valores de sus variables, incluido el contador de programa.

CONSIDERANDO EL RECEPTOR DEL PROTOCOLO 3, ¿CUÁNTOS ESTADOS SE PUEDEN ABSTRAER?

Podemos abstraer dos estados importantes de todos los posibles: en espera de la trama 0 y en espera de la trama 1

¿CÓMO PUEDEN CONSIDERAR  TODOS LOS DEMÁS ESTADOS?

Pueden considerarse como transitorios: pasos en el camino hacia uno de los estados principales.

¿PARA QUÉ SE ESCOGEN LOS ESTADOS?

Para que sean aquellos instantes en que la máquina de protocolo está esperando que ocurra el siguiente evento.

El número de estados es entonces 2n, donde n es el número de bits necesarios para representar todas las variables combinadas.

ESTADO DEL SISTEMA COMPLETO:

Es la combinación de todos los estados de las dos máquinas de protocolos y del canal.

EL PROTOCOLO 3 TIENE CUATRO POSIBLES ESTADOS, ¿CUÁLES SON?

-una trama cero o una trama 1  viajando del emisor al receptor

- una trama de confirmación de recepción que va en el otro sentido o un canal vacío

¿CUÁNDO UNA TRAMA PERMANECE “EN EL CANAL”?

Hasta que la máquina de protocolo ejecuta FromPhysicalLayer y la procesa.

DE CADA ESTADO HAY CERO O MÁS TRANSICIONES POSIBLES A OTROS ESTADOS. PARA UNA MÁQUINA DE PROTOCOLO, PODRÍA OCURRIR UNA TRANSICIÓN AL ENVIAR UNA TRAMA, COMO:

-Al llegar una trama,

-Al terminar un temporizador

-Al ocurrir una interrupción

¿CUÁLES SON LOS EVENTOS TÍPICOS PARA EL CANAL?

 Son la inserción de una trama nueva en el canal por una máquina de protocolo, la entrega de una trama a una máquina de protocolo o la pérdida de una trama debido a una ráfaga de ruido.

ESTADO INICIAL:

Corresponde a la descripción del sistema cuando comienza a funcionar, o en algún punto conveniente poco después.

¿USANDO QUÉ TEORÍA ES POSIBLE DETERMINAR LOS ESTADOS QUE SON ALCANZABLES Y LOS QUE NO?

 Análisis de asequibilidad. Este análisis puede ser útil para determinar si un protocolo es correcto o no.

UN MODELO DE MÁQUINA DE ESTADOS FINITOS DE UN PROTOCOLO SE PUEDE CONSIDERAR COMO UN CUÁDRUPLE (S, M, I, T), DONDE:

 S es el conjunto de estados en que pueden estar los procesos y el canal.

M es el conjunto de tramas que pueden intercambiarse a través del canal.

 I es el conjunto de estados iniciales de los procesos.

T es el conjunto de transiciones entre los estados.

¿QUÉ PUEDE CAUSAR UN EVENTO?

 Puede causar que uno de los procesos o el canal emprenda una acción y cambie a un estado nuevo.

¿PARA QUÉ SIRVE EL  ANÁLISIS DE ASEQUIBILIDAD?

 Puede servir para detectar una variedad de errores en la especificación del protocolo

SE UTILIZAN TRES CARACTERES PARA ETIQUETAR CADA ESTADO.

-SRC, donde S es 0 o 1 y corresponde a la trama que el emisor está tratando de enviar;

-R también es 0 o 1 y corresponde a la trama que el receptor espera

-C es 0, 1, A o vacío (−) y corresponde al estado del canal.

PROTOCOLO 3. 

EN LA FIGURA 3-21 SE MUESTRAN NUEVE TIPOS DE TRANSICIONES:

·         La transición 0 consiste en la pérdida del contenido del cana

·         La transición 1 consiste en que el canal entregue de manera correcta el paquete 0 al receptor, y que éste cambie a continuación su estado para esperar la trama 1.

·         las transiciones 1, 2, 3 y 4 se repiten en orden una y otra vez. En cada ciclo se entregan dos paquetes, regresando el emisor al estado original de tratar de enviar una trama nueva con un número de secuencia 0

·         7 y 5 u 8 y 6, para reparar el daño.

PROPIEDADES QUE DEBE TENER UN PROTOCOLO CON UN NÚMERO DE SECUENCIA DE 1 BIT

 Sin importar la secuencia de eventos que ocurra, el receptor nunca debe entregar dos paquetes impares sin haber intervenido un paquete par, y viceversa.

Otro requisito semejante es que no debe haber rutas en las que el emisor pueda cambiar de estado dos, mientras el estado del receptor permanezca constante.

DE EXISTIR LA RUTA EN LA SECUENCIA CORRESPONDIENTE, ¿QUÉ PASARÍA?

 Se perderían dos tramas sin posibilidad de recuperación y sin que el receptor se diera cuenta.

PROPIEDAD IMPORTANTE DE UN PROTOCOLO Y EN QUÉ CONSISTE

 Ausencia de bloqueos irreversibles. Un bloqueo irreversible es una situación en la que el protocolo no puede seguir avanzando, sea cual sea la secuencia de eventos que ocurra.

EN TÉRMINOS DEL MODELO GRÁFICO, ¿DE QUÉ SE CARACTERIZA?

 Un bloqueo irreversible se caracteriza por la existencia de un subconjunto de estados que es alcanzable desde el estado inicial y que tiene dos propiedades:

1. No hay transición hacia fuera del subconjunto.

2. No hay transiciones en el subconjunto que causen un avance.

MODELOS DE RED DE PETRI

 Una red de Petri tiene cuatro elementos básicos: lugares, transiciones, arcos y tokens.

Un lugar representa un estado en el que puede estar parte del sistema. En la figura 3-22 se muestra una red de Petri con dos lugares, A y B, que aparecen como círculos. El sistema actualmente está en el estado A, indicado por el token (punto grueso) en el lugar A. Se utiliza una barra horizontal o vertical para indicar una transición. Cada transición tiene cero o más arcos de entrada, que llegan de sus lugares de entrada, y cero o más arcos de salida, que van a sus lugares de salida.

¿PARA QUÉ PUEDEN SERVIR LAS REDES PETRI?

 Las redes de Petri pueden servir para detectar fallas de protocolo de una manera parecida a como se hace con máquinas de estados finitos.