Uppaal y

Facultad Regional Tucumán
Universidad Tecnológica Nacional

Materia: Sistemas de Tiempo Real
Profesor: Ing. Pablo Rovarini
Alumno: Vides, Luis Sebastián

TEMA:

Autómatas Temporizados
y Model-checking

PROTOCOLO DE ENLACE
DE DATOS SIMPLE

Un caso de estudio usando UPPAAL

-2003-

Autómatas temporizados y UPPAAL

Índice
• Autómatas temporizados.
• El model checkerUPPAAL.
• Ejemplo.

1 Autómatas temporizados

Relojes
Un autómata temporizado es un autómata finito equipado con un conjunto finito de variables reales positivas llamadas relojes.

El estado de un autómata temporizado viene dado por:
la localización del autómata finito
el valor de los relojes

Algunas características de los relojes son:
Todos cuentan el tiempo a la mismavelocidad
Pueden ser inicializados cuando se realiza una transición.
Su valor indica el tiempo trascurrido desde la última actualización.
Pueden utilizarse para imponer restricciones sobre la habilitación de una transición.

Restricciones de reloj
Sea C un conjunto de relojes, con x, y [pic] C. El conjunto de restricciones de reloj sobre C, [pic](C), se define como sigue:

[pic]
donde c [pic]N y [pic].

Utilizaremos expresiones abreviadas como:
x [pic] c en lugar de [pic](x < c)
x = c en lugar de x [pic] c ^ x [pic] c

Definición de autómata temporizado

Es una tupla (L; l0; E; Label;C; clocks; guard; inv) donde:
• L, conjunto finito no vacío de localizaciones, siendo l0 la localización inicial.
• E [pic], conjunto de arcos.
• Label : L ( 2AP , función queasigna a cada l [pic] L el conjunto de proposiciones atómicas Label(l).
• C, conjunto finito de relojes.
• clocks : E ( 2C, función que asigna a cada arco e [pic] E un conjunto de relojes clocks(e) que deben ser inicializados.
• guard : E ( [pic](C), función que etiqueta cada arco e [pic] E con una restricción de reloj guard(e)
• inv : L ( [pic] (C), función que asigna a un l [pic]L una restricción sobre el tiempo que puede pasar en l (invariante).
[pic]

Dos localizaciones con etiquetas on y off (localización inicial).
Relojes: x e y.
Reset de relojes: reloj x siempre, reloj y en transición off-on
Guardas: x [pic] 2 e y = 9.
No hay invariantes.

[pic]
2 El model checker UPPAAL

Introducción

UPPAAL es un conjunto de herramientas que permite la validación(vía simulación gráfica) y la verificación (vía model checking) de sistemas de tiempo real.
La idea es:
• modelar un sistema mediante autómatas temporizados y
• verificar propiedades sobre él mediante una lógica similar a TCTL.

Especificación de sistemas

Para especificar un sistema en UPPAAL es necesario realizar las siguientes operaciones:
1. Definir las plantillas de procesos.2. Declarar las variables locales a cada plantilla.
3. Declarar las variables globales.
4. Definir los procesos en base a las plantillas previamente definidas
5. Especificar el sistema indicando que procesos se ejecutan concurrentemente.

Tipos de datos
Pueden utilizarse los siguientes tipos de datos:
• Constantes: const true 1;
• Variables enteras: int a;
•Variables enteras acotadas: int[0,2] activado;
• Arrays de variables enteras: int a[3];
• Canales (sólo globales): chan canal1;
• Canales urgentes (sólo globales): urgent chan canal1;
• Relojes: clock x;

Puede inicializarse una variable en el momento de su declaración:
int[0,10] a:=5.

Atributos de objetos
Una plantilla de proceso se compone de dos objetos principales:localizaciones y transiciones.
Las localizaciones tienen los siguientes atributos:
• Un nombre (obligatorio)
• Un invariante
• Una marca de estado inicial
• Una marca de estado committed: la localización debe abandonarse inmediatamente
• Una marca de estado urgent: no debe pasar el tiempo pero se permite interleaving con localizaciones normales de otros procesos....