Inicio

Generalidades

Ejercicios

Talleres

Proyecto

 Criterios de Corrección

 El objetivo principal del lenguaje PROMELA es validar, y no implementar.

• Para validar un diseño, es necesario especificar de manera clara y precisa lo que entendemos por un diseño correcto.

• Un diseño puede ser considerado correcto sólo para un conjunto específico de criterios de corrección.

• Necesitamos de un formalismo para especificar los criterios de corrección.

• Entre más expresiva sea nuestra notación, menos útil será en la práctica.

• Por lo tanto, los criterios de corrección que pueden ser especificados en PROMELA han sido escogidos cuidadosamente.

 Razonamiento sobre el comportamiento

• Formalizamos los criterios de corrección como afirmaciones sobre el comportamiento de un modelo de validación en PROMELA.

• Un comportamiento es: Inevitable o imposible.

 Los criterios de corrección que pueden ser expresados en PROMELA definen comportamientos considerados como imposibles.

 Justificación

 Para afirmar que un comportamiento es inevitable, por ejemplo, podemos estipular que todos los comportamientos posibles que nos alejan de él, son imposibles.

 Definiciones en PROMELA

• El comportamiento de un modelo de validación se define como el conjunto de todas las secuencias de ejecución posibles.

• Una secuencia de ejecución es simplemente un conjunto finito de estados ordenados.

• Un estado está dado por el valor de todas las variables locales y globales, puntos de control de flujo de los procesos en ejecución y por el contenido de todos los mensajes de comunicación.

• Un conjunto finito de estados ordenados es considerado válido para un modelo M dado si satisface los siguientes criterios:

1. El estado inicial de la secuencia, por ejemplo, el estado 1, es el estado inicial de M, con todas las variables inicializadas en 0, todos los canales de comunicación vacíos y sólo con el proceso init activo.

2. Si M es colocado en el estado i, existe por lo menos un enunciado ejecutable que lo llevará al estado i + 1.

 Secuencias Especiales: Terminales y Cíclicas

• Una secuencia es terminal si ningún estado aparece más de una vez en la secuencia y el modelo M no contiene enunciados ejecutables una vez alcanzado el último estado de la secuencia.

• Una secuencia es cíclica si todos los estados menos el último son diferentes, y este último es igual a alguno de los estados precedentes.

• Secuencias cíclicas definen ejecuciones potencialmente infinitas.

• Las secuencias terminales y cíclicas que pueden ser generadas al ejecutar un modelo en PROMELA, definen juntas el comportamiento del sistema para ese modelo.

• La unión de todos los estados incluidos en el comportamiento del sistema, define el conjunto de estados alcanzables del modelo.

 Criterios de validación

• Aserciones:  assert ( condicion)

• Invariantes del sistema:  proctype monitor () { assert (invariante) }

Ejemplo: Semáforos Dijkstra

#define p 0
#define v 1
chan semaf = [0] of { bit }
proctype dijkstra () { 
do
  :: semaf ! p -> semaf ? v
od
}
proctype user () {    
    semaf ? p;
    /* Sección crítica */
    semaf ! v
    /* Sección no crítica */
}
init {
    atomic {
            run dijkstra();
            run user(); run user(); run user();
    }
}

• El semáforo garantiza acceso exclusivo a la región crítica de cada proceso user.

• Se puede modificar el proceso user de tal manera que la variable global count contenga el número de procesos que se encuentran en su sección crítica:

byte count;
proctype user() {
 semaf ? p
    count = count + 1;  /* Sección crítica */
    count = count - 1;
 semaf ! v 
   /* Sección no crítica */
}

• La siguiente invariante del sistema puede ser utilizada para verificar el funcionamiento correcto del semáforo:
  
  proctype monitor () {    
      assert ( count == 0 || count == 1 )
  }
   
  init {
      atomic {
              run dijkstra();  run monitor();
              run user(); run user(); run user();
      }
  }
   

• Deadlocks:

proctype dijkstra () { 
end: do
        :: semaf ! p -> semaf ? v
       od
}

• Ciclos erróneos: Existen dos propiedades sobre las secuencias cíclicas correspondientes a dos tipos estándares de criterios de corrección. Las dos propiedades se basan en el marcado explícito de estados en el modelo de validación.

• Ciclos sin progresión:

proctype dijkstra () {    
 end :  do
            ::    semaf  !  p ->
 progress :  semaf  ? v
          od
}

• Livelocks:

proctype dijkstra () {    
 end :  do
            ::    semaf  !  p ->
 accept :     semaf  ? v
          od
}

• Exigencias temporales:

never {    
         do
            ::  skip
          od -> P -> ! Q
}

 Conclusiones

• Se ha introducido el resto de las directivas de validación PROMELA.

• Estas directivas están relacionadas con la especificación de los criterior de corrección para un modelo:  Enunciados de aserción, Etiquetas end, progress y accept,  Exigencia temporal never.

• Es prácticamente imposible verificar manualmente requerimientos de corrección.

• El comportamiento de inclusive protocolos simples es bastante complejo.

• Herramientas automatizadas como PROMELA son imprescindibles, no sólo para expresar los requerimientos de corrección del diseño de un protocolo, sino también para validarlos de manera confiable.

 Ejercicios:

1. Explique los principales criterios de validación.

2. ¿Explique los ejemplos de Deadlocks y Livelocks?

3. ¿Cuáles son las dos propiedades sobre las secuencias cíclicas correspondientes a los dos tipos estándares de criterios de corrección?

4. ¿Cómo se hace referencia a instancias de procesos en PROMELA?

5. ¿Cómo se hace referencia a las variables locales de procesos?