Inicio

Generalidades

Ejercicios

Talleres

Proyecto

 Validación de Protocolos

 Se necesita verificar la consistencia lógica de una especificación formal. La especificación es formalizada como un modelo de validación en PROMELA, por ejemplo.

 Método Manual de Prueba

• Considere un sistema simple de transmisión con un transmisor S y un receptor R.

• El proceso S envía mensajes al proceso R a través de un medio no confiable de transmisión.

• Cada mensaje transmitido lleva un número de secuencia, incialmente igual a 1 e incrementado en 1 después de cada transmisión.

• El receptor reconoce el mensaje recibido mediante la transmisión del número de secuencia a través de un canal similar.

• El receptor almacena el número de secuencia más grande que ha recibido correctamente en su variable local B.

• El emisor guarda en la variable A el número de secuencia más grande que R ha recibido correctamente.

• Inicialmente, A = B = 0.

En PROMELA:

#define W cte_positiva
chan R = [W] of { int }
chan S = [W] of { bit }
mtype = { mesg, ack } 

proctype S () {    
    int A = 0;
    do
     :: R ! mesg (A + rand () % W)  /* S1 */
     :: S ? ack(A)  /* S2 */
    od
}

proctype R () {    
    int B = 0, b;
    do
     :: S ! ack (B)   /* R1 */
     :: atomic {       /* R2 */
                R ? mesg (b);
                B = fct (b, B);
}
    od
}
 

• fct (b, B) memoriza la recepción del mensaje con número de secuencia igual a b y regresa un valor X ≥ B para el cual garantiza que todos los mensajes con número de secuencia menor o igual a X  fueron grabados previamente por  fct ().

 Discusión sobre los Métodos Manuales

• Basados en la noción de estados invariantes.

• Contrariamente a los métodos usados en sistemas de validación automatizados, el método manual no se basa en la inspección de estados del sistema alcanzables, sino en la inspección de transmisiones de estado.

• Normalmente hay menos transiciones de estado que estados del sistema alcanzables.

• Sin embargo, puede requerir demasiado esfuerzo verificar que una transición no puede invalidar ninguna de las invariantes del sistema.

• Lo anterior implica que es un método ineficiente para sistemas grandes, por lo cual se requieren herramientas automatizadas para la construcción de pruebas.

 Métodos de Validación Automatizados

Algoritmos de Análisis de Estados Alcanzables

• Este tipo de algoritmos trata de generar e inspeccionar todos los estados de un sistema distribuido que son alcanzables a partir de un estado inicial.

• Existen tres tipos: Búsqueda completa (sistemas con hasta 10⁵  estados), Búsqueda parcial controlada (sistemas con hasta 10⁸  estados), Simulación aleatoria (sistemas aún más grandes).

El intérprete SPIN puede ser utilizado en las tres modalidades: Simulaciones aleatorias, Búsqueda parcial y Búsqueda exhaustiva.

Método 1: Búsqueda completa o exhaustiva del espacio de estados

• Se lleva a cabo un análisis de todos los estados alcanzables y los no alcanzables.

• Se separan los estados alcanzables y los no alcanzables.

• Cada estado alcanzable y toda secuencia de estados alcanzables pueden ser verificados por un conjunto de criterios de corrección.

• Ejemplos de criterios de corrección: Ausencia de deadlocks, saturación de buffers, requerimientos temporales, invariantes del sistema, etc.

 ALGORITMO DE BÚSQUEDA COMPLETA DEL ESPACIO DE ESTADOS:

start(){
    W = { initial_state };  /* estados por analizar */
    A = { };                    /* estados previamente analizados */
    analyze();                 
}
analyze() {                   /* Búsqueda exhaustiva */
    if ( W is empty ) return;
         q = last element from W;
         add q to A;
         if (q == error_state)
             report_error();
         else

         { for each succesor state s of q    
                 if (s is not in A or W){
                    add s to W;
                    analyze();
                 }
         }
           delete q from W;
}
 

 Discusión sobre el Método de Búsqueda Exhaustiva

• El problema principal consiste en la capacidad de memoria disponible así como en la velocidad de procesamiento.

• Considere un protocolo con dos procesos, cada uno con 100 posibles estados, un canal de comunicación y 5 variables locales. Ambos canales están limitados a 5 entradas cada uno, en donde el número de mensajes diferentes a intercambiar es 10. Los valores distintos para las variables locales está limitada a 10.

• Búsqueda exhaustiva: sistemas con hasta 10⁵  estados alcanzables.

Método 2: Búsqueda Parcial Controlada

• Basada en la premisa de que en la mayoría de los casos prácticos, el número máximo de estados que pueden ser analizados, A, es sólo una fracción del número total de los estados alcanzables R.

• Una búsqueda parcial controlada tiene los siguientes objetivos:

          1. Analizar exactamente A estados.

          2. Seleccionar los A estados del conjunto completo de estados alcanzables R, de tal manera que la mayoría de las funcionalidades del protocolo sean probadas.

          3. Seleccionar los A estados de manera que la calidad de búsqueda, como la probabilidad de encontrar algún error dado, sea mejor que la cobertura A/R.

 ALGORITMO DE BÚSQUEDA PARCIAL CONTROLADA:

analyze() {                   /* Búsqueda parcial controlada */
    if ( W is empty ) return;
         q = last element from W;
         add q to A;
         if (q == error_state)
             report_error();
         else

         { for some succesor state s of q    
                 if (s is not in A or W){
                    add s to W;
                    analyze();
                 }
         }
           delete q from W;
}
 La selección de los estados sucesores puede ser hecha basada en una heurística para favorecer ejecuciones que revelen, con una probabilidad alta, errores de diseño. Los siguientes métodos son usados para establecer los criterios de selección: Límite de profundidad, Búsqueda dispersa, Búsqueda probabilística, Orden parcial y Selección aleatoria.

- Límite de profundidad: Se establece un límite en la longitud de las secuencias que serán analizadas.  Limita la búsqueda a un subconjunto representativo de comportamientos.

- Búsqueda probabilística: Los estados son analizados, según su probabilidad de ocurrencia, en orden decreciente.  Las transiciones del sistema son etiquetadas con una alta o baja probabilidad de ocurrencia, lo cual sirve como criterio de selección.

- Orden parcial: Los procesos son clasificados en procesos de alta y baja prioridad.  Una transición perteneciente a un proceso de alta prioridad es favorecida a una transición de un proceso de baja prioridad.

- Selección aleatoria: No se realiza ningún esfuerzo para predecir los estados del sistema en los cuales se encontrarán los errores más probables.  Este método es el más sencillo de implementar y el que produce una búsqueda con la más alta calidad.

 Discusión sobre los Métodos de Búsqueda Parcial Controlada

•  Las primeras tres técnicas para controlar la búsqueda parcial tienen el siguiente problema en común: tratan de predecir dónde pueden ser encontrados los errores del protocolo.

• A pesar de que estos métodos reducen el número de estados del sistema analizados, estos están limitados ya en la práctica a sistemas con hasta 10⁸  estados.

• Corolario de la Ley de Murphy:

 Los errores se esconden muy probablemente en donde el diseñador o el validador han decidido no buscar.

Método 3: Simulaciones Aleatorias

• Utilizado para sistemas con más de 10⁸  estados.

• El algoritmo descarta los conjuntos A y W y explora el espacio de estados usando la técnica de "Baco".

 ALGORITMO DE SIMULACIÓN ALEATORIA:

analyze() {                   /* Simulación aleatoria */
         q = initial state;
         while (1){
             if (q is error_state){
                 report_error();
                 q = initial state;

             { else
                 q = a succesor state of q;
                   
         }
}

• El algoritmo funciona de manera independiente al tamaño y complejidad del sistema modelado (inclusive sistemas de tamaño infinito).

 ALGORITMO Supertrace:

• La implementación en C del algoritmo forma parte del intérprete Spin.

• Recuérdese que Spin ofrece las tres modalidades: Búsqueda exhaustiva, Búsqueda parcial controlada y Simulación aleatoria.

 Ejercicios:

1. Mencione cuatro ejemplos de criterios de corrección.

2. ¿Cuáles son los métodos usados para establecer los criterios de selección?

3. ¿Qué es una búsqueda dispersa?

4. ¿Para qué se utiliza el spin en PROMELA?

5. ¿Qué técnica de búsqueda utiliza el algoritmo Supertrace?