Inicio

Generalidades

Ejercicios

Talleres

Proyecto

 Modelos de Validación

 Un modelo de validación define las interacciones de procesos en un sistema distribuido.

 Se definen los modelos de validación en términos de tres tipos de objetos:

1. Procesos

2. Canales

3. Variables

 PROMELA

 Es un lenguaje usado para describir modelos de validación. PROMELA fue creado en 1980 y es un subconjunto de C y OCAN.

 Enunciados Ejecutables

• En PROMELA no hay diferencias entre condiciones y enunciados.

• Los enunciados son ejecutables o bloqueantes.

• El estado ejecutable de un enunciado representa el medio principal de sincronización.

• Un proceso puede esperar a que un evento suceda hasta que un enunciado se vuelva ejecutable. Por ejemplo, en lugar de escribir:

          while (a != b) skip /* wait for == b */

 En PROMELA se tiene el mismo efecto con el siguiente enunciado:

          (a == b)

• La condición es ejecutada sólo si es verdadera.

• Si la condición es falsa, la ejecución es bloqueada hasta que la condición sea verdadera.

• La asignación a variables siempre es ejecutable.

 Variables y Tipos de Datos

• Las variables pueden ser globales o locales a un proceso.

• Una variable puede ser de alguno de los siguientes tipos predefinidos: bit, bool, byte, short, int, chan.

• Un canal es un objeto que puede almacenar un conjunto de valores agrupados en estructuras definidas por el usuario.

 Arreglos

          byte state [N]

 Procesos

 proctype  A()  {

               byte state;

               state = 3

 }

 ';' y '->' son separadores equivalentes de enunciados. Ejemplo:

        byte state = 2;

        proctype A () { (state == 1) -> state = 3 }

        proctype B () { state = state - 1 }

 Proceso init

• Equivalente a la función main() de lenguaje C.

• La especificación más pequeña posible en PROMELA es:

          init  { skip }

 Otros ejemplos,

          init  { printf  ( "Hola, mis pupilos! \n" ) }

 Para instanciar los procesos A y B:

          init  { run A ();  run B () }

• El proceso init lanza dos procesos, que serán ejecutados de manera concurrente.

• En éste caso, el proceso init termina después de haber lanzado el segundo proceso.

• run instancia una copia del proceso dado como operando.

• run no espera a que el proceso termine.

• run es un enunciado ejecutable y regresa un número positivo (pid) sólo si el proceso pudo ser instanciado.

• Es no ejecutable y regresa 0 si el proceso no pudo ser instanciado.

 Paso de Parámetros a un Nuevo Proceso

 proctype  A  (byte state; short set)  {

               ( state == 1) -> state = set }

 init  { run A (1, 3) }

• Sólo valores de cualquiera de los tipos base, pueden ser pasados como parámetros.

• No es posible pasar arreglos ni procesos.

• run puede ser usado en cualquier proceso para crear nuevos procesos.

• Un proceso muere cuando termina, es decir, cuando alcanza el final de su cuerpo, siempre y cuando todos sus procesos hijos hayan terminado.

 Canales de comunicación

• Usados para modelar la transferencia de información entre procesos.

• Pueden ser locales o globales.

          chan  a, b;  chan  c  [3]

 Define a y b como identificadores de canal; c  como arreglo de identificadores de canal.  La declaración de un canal puede tener un inicializador. Ejemplos:

          1.  chan a = [16] of { short }   El canal puede almacenar hasta 16 mensajes de tipo short.

          2.  chan c [3] = [4] of { byte }

         3.  chan qname = [2] of { byte, int, chan }

 Envío de Mensajes

          qname  !  expr

 Envía el valor de la expresión expr a través del canal qname; lo coloca en el buffer asociado al canal qname (política FIFO).

 Recepción de Mensajes

          qname  ?  msg

 

byte

int

chan

byte

int

chan

 Recupera el primer mensaje en el buffer asociado al canal qname y almacena su valor en la variable msg.

 Envío y Recepción de Mensajes estructurados

          qname  !  expr1, expr2, expr3

          qname  ?  var1, var2, var3

 Comunicación Síncrona (Rendezvous)

          chan  port = [0]  of  { byte }

• Estamos definiendo un tamaño de buffer para el canal port igual a 0, por lo que no es posible almacenar mensajes.

• La comunicación es síncrona y binaria; sólo dos procesos, un transmisor y otro receptor son sincronizados.

 Control de Flujo

• Selección case.

• Repetición.

• Jumps incondicionales.

 Selección Case

 if
   :: (a != b) -> opcion1
   :: (a == b) -> opcion2
 fi

<> Sólo una secuencia de enunciados (opción1 u opción2) es ejecutada.
<> Una secuencia es seleccionada sólo si su primer enunciado es ejecutable.
<> El primer enunciado es llamado guardia.
<> Si más de un guardia es ejecutable, una sola secuencia de las asociadas a dichos guardias, es seleccionada de manera aleatoria.
<> Si ningún guardia es ejecutable, el proceso se bloquea hasta que por lo menos uno de ellos pueda ser seleccionado.

Ejemplo 1:

#define a 1
#define b 2
chan ch = [1] of { byte }
proctype A () { ch ! a }
proctype B () { ch ! b }
proctype C () {
if
  :: ch ? a
  :: ch ? b
fi
}
init { atomic { run A(); run B(); run C () }


Ejemplo 2:

byte count;
proctype counter() {
if
  :: count = count + 1
  :: count = count - 1
fi
}

 Repetición

 El siguiente ciclo incrementa o decrementa la variable de manera aleatoria:

byte count;
proctype counter() {
 do
    :: count = count + 1
    :: count = count - 1
    :: (count == 0) -> break
 od
}

<> El ciclo puede ser roto con el enunciado break cuando count es igual a 0.
<> Puede no terminar ya que las otras dos opciones son seleccionables.

proctype counter() {
 do
   :: (count != 0) ->
      if
        :: count = count + 1
        :: count = count - 1
      fi
   :: (count == 0) -> break
 od
}

 Saltos incondicionales (jumps)

proctype Euclid (int x, y) {
 do
    :: (x > y) -> x = x - y
    :: (x < y) -> x = y - x
    :: (x == y) -> goto done
 od
done:
    skip
}

 Funciones, Procedimientos y Recursión

proctype fact (int n; chan p) {
 int result;
 if
   :: (n <= 1) p ! 1
   :: (n >= 2) ->
   chan child = [1] of { int };
   run fact (n - 1, child);
   child ? result;
   p ! n * result
 fi
}
init
{ int result;
  chan child = [1] of { int };
  run fact (3, child);
  child ? result;
  printf ("Resultado: %d \n", result)
}
 

 Definición de los Tipos de Mensaje

       mtype = {ack, nak, err, next, accept}

Equivalente a:

#define ack 1
#define nack 2
#define err 3
#define next 4
#define accept 5
 

 Temporizadores

proctype watchdog () {
 do
   :: timeout  -> guard  !  reset
 od
}

• timeout es una condición predefinida que se vuelve verdadera sólo cuando ningún otro enunciado en el sistema distribuido es ejecutable.

• No modela errores causados por la expiración prematura del temporizador en un sistema real.

 Tipos de Enunciados

• Asignación y condición.

• Selección y repetición.

• send y receive.

• goto y break.

• timeout.

 run y len no son enunciados, sino operadores unarios que pueden ser usados en asignaciones y condiciones. skip es un seudo enunciado.

 Ejercicios:

1. ¿Cuáles son los tres tipos de objetos que definen los modelos de validación?

2. ¿Cuál es el equivalente a la función main() de C en el lenguaje PROMELA?

3. ¿A qué se refiere el término Rendezvous?

4. ¿Cómo realiza PROMELA el control de flujo?

5. ¿Cómo implementa un temporizador?

6. ¿Cómo se definen en PROMELA los tipos de mensaje?

7. ¿Cuáles son los tipos básicos de enunciados definidos en PROMELA?