Vai alla Home Page About me Courseware Federica Living Library Federica Federica Podstudio Virtual Campus 3D Le Miniguide all'orientamento Gli eBook di Federica La Corte in Rete
 
 
Il Corso Le lezioni del Corso La Cattedra
 
Materiali di approfondimento Risorse Web Il Podcast di questa lezione

Adriano Peron » 18.Il sistema di verifica UPPAAL


Temi della lezione

Introduzione alla verifica di sistemi real-time in UPPAL:

  • Descrizione del sistema
    • Funzionalità
    • Esempio di specifica
  • Reti di automi temporizzati
    • Sintassi e semantica
  • Facilitazioni aggiuntive nella specifica
    • Uso di variabili condivise
    • Transizioni urgenti e committed

Linguaggio di specifica in UPPAAL

Estensione degli automi temporizzati con le seguenti caratteristiche.

Composizione parallela di automi temporizzati (Rete di Timed automata).

Canali di comunicazione tra componenti parallele:

  • canali per comunicazione sincrona a rendez-vous (c! si sincronizza con un unico ricevente c?);
  • canali per broadcast (c! si sincronizza con un numero arbitrario di riceventi c?).

Uso di variabili condivise:

  • variabili intere limitate (modificabili con le comuni operazioni aritmetiche);
  • array di orologi, canali, interi, costanti.

Templates: automi definiti in modo parametrico che consentono l’istanziazione semplice di copie del medesimo automa.

Costrutti di Urgenza per evitare ritardi non necessari nell’esecuzione:

  • sincronizzazioni urgenti;
  • locazioni urgenti;
  • locazioni committed.

Reti di Automi temporizzati

Per semplicità verrà considerata formalmente solo l’estensione degli automi temporizzati con parallelismo e comunicazione sincrona mediante rendez-vous.

Una rete di automi temporizzati è una collezione di automi temporizzati che condivide l’insieme degli orologi e l’alfabeto.

XTA = TA_1\ \mid\  TA_2\ \mid\ \ldots \mid\ TA_n, \mbox{ dove }

TA_i = \langle\Sigma ,Loc_i, Loc_{i,0}, C, \delta_i ,Inv_i, F_i \rangle \mbox{ con } 1 \leq i \leq n.

La semantica delle reti di automi estende naturalmente al caso parallelo la semantica degli automi temporizzati:

  • tutte le componenti parallele avanzano nel tempo simultaneamente e concordemente rispettando gli invarianti temporali di tutte le locazioni correnti;
  • una componente che fa una azione interna può avanzare in modo asincrono rispetto alle altre;
  • coppie di transizioni complementari comunicanti avanzano sincronamente.

Semantica delle reti di automi temporizzati

La semantica della rete XTA di automi temporizzati viene data definendo un LTS

\langle S_0, S, \Delta \rangle

Lo stato raccoglie informazioni sul controllo di tutte le componenti e sulla valutazione corrente degli orologi (comune a tutte le componenti).

S \subseteq Loc_1 \times Loc_2 \times \ldots \times Loc_n \times Val(C)

Gli stati iniziali hanno valutazione dei clock a tempo zero.

S_0 = Loc_{1,0} \times Loc_{2,0} \times \ldots \times Loc_{n,0}\times \{v_0\}

con v_0(x)=0 \mbox{ per ogni } x \in C

\Delta \subseteq S \times \Sigma_{\tau}\times S

L’insieme di transizioni è l’unione dei tre seguenti insiemi di transizioni.

Semantica delle reti di automi temporizzati (segue)

1) Il tempo avanza di un quantità t uniformemente per tutte le componenti:

\{\langle(\langle l_1, \ldots ,l_n \rangle,v),\tau(t),(\langle l_1, \ldots ,l_n \rangle,v+t) \rangle : t\in {\cal Q}^{\geq 0}, (\langle l_1, \ldots ,l_n \rangle,v) \in S, \bigwedge^n_{i=1} v+t \models Inv(l_i)\}

(2) Una componente fa una mossa interna asincrona

\begin{array}{ll}\{\langle(\langle l_1, \ldots ,l_i, \ldots ,l_n \rangle,v),\tau,&(\langle l_1, \ldots ,l'_i, \ldots ,l_n \rangle,v-Y) \rangle : \\& \langle l_i,\tau,\phi,Y,l'_i\rangle \in \delta_i, \\& (\langle l_1, \ldots ,l_i, \ldots ,l_n \rangle,v) \in S, \\& v \models \phi, \\& v-Y \models Inv_i(l'_i)\\& v-Y \models \bigwedge_{1 \leq j \leq i-1}Inv_j(l_j)\wedge \bigwedge_ {i+1 \leq j \leq n}Inv_j\}\end{array}

Semantica delle reti di automi temporizzati (segue)

(2) Due componenti fanno una mossa sincrona di comunicazione

\begin{array}{ll}\{\langle(\langle l_1, \ldots ,l_i, \ldots ,l_n \rangle,v),\tau, & (\langle l_1, \ldots ,l'_i, \ldots ,l_n \rangle,v-Y) \rangle : \\ & \langle l_i,c_i,\phi_i,Y_i,l'_i\rangle \in \delta_i,\langle l_j,c_j,\phi_j,Y_j,l'_j\rangle \in \delta_j, 1 \leq i < j \leq n\\& c_i=a!, c_j=a? \mbox{ oppure } c_i=a?, c_j=a! \mbox{ per qualche } a\\& (\langle l_1, \ldots ,l_i, \ldots ,l_n \rangle,v) \in S, \\& v \models \phi_i \wedge \phi_j, \\& v-(Y_i\cup Y_j) \models Inv_i(l'_i)\wedge Inv_j(l'_j)\\& v-(Y_i \cup Y_j) \models \bigwedge_{1\leq l \leq n, l\neq i, l \neq j}Inv_l(l_l)\end{array}

Gestione urgenza (segue)

Sono possibili tre tipi distinti di locazioni:

(1) Locazioni normali

  • Con o senza invarianti

(2) Locazioni urgenti

  • Marcate da U, il tempo non può avanzare quando si permane in una locazione urgente.
  • Rappresentano attività da svolgere a tempo zero

Esempio
Le transizioni h_1 \mbox{ e } h_3 debbono scattare simultaneamente in un istante 0 \leq t \leq 1
Dopo il loro scatto non vi può essere avanzamento temporale perché lo stato contiene una componente urgente.
La transizione h_4 deve eseguita al tempo t.
La transizione h_2 può essere eseguita nell’intervallo [t,2].

Fig.1 Locazioni urgenti.

Fig.1 Locazioni urgenti.


Gestione urgenza (segue)

Locazioni committed
Marcate da C, il tempo non può avanzare quando si permane in una locazione C
Le transizioni che hanno una locazione C come sorgente hanno la priorità sulle transizioni che hanno come sorgente locazioni normali e urgenti.

Esempio
Si assuma che la transizione h_1 scatti per prima seguita dalla sincronizzazione di h_2 \mbox{ e } h_3.

h_5 \mbox{ e } h_6 hanno la priorità su h_4

Le sequenze possibili sono:

  • h_5, h_6, h_4 oppure
  • h_6, h_5, h_4.
Fig.2 Locazioni committed.

Fig.2 Locazioni committed.


Specifica della rete di automi

La definizione della rete di automi temporizzati può essere fatta graficamente usando una GUI per la composizione grafica degli automi.

Rispetto a SPIN si conserva la possibilità di mantenere la natura grafica della rappresentazione stato-transizione del sistema)
L’utente compone manualmente la specifica.

Testualmente usando una definizione dell’automa in una codifica in linguaggio XML.

La rappresentazione XML permette la memorizzazione e lo scambio delle specifiche,
La specifica può essere sintetizzata in formato testuale come traduzione di specifiche scritte in linguaggi di più alto livello.

Fig.3 Input della specifica.

Fig.3 Input della specifica.


Editor grafico


Rappresentazione XML dell’automa


Editor grafico: dichiarazioni globali

Contine la dichiarazione di elementi globali:

  • orologi;
  • costanti;
  • nomi e tipi di canali;
  • variabili condivise.
Fig.6 Dichiarazioni globali.

Fig.6 Dichiarazioni globali.


Editor grafico: Template

Templates: contiene la dichiarazione degli Automi Temporizzati parametrizzati. Un template può avere dichiarazioni locali di variabili, canali e costanti.

Fig.7 Dichiarazioni template.

Fig.7 Dichiarazioni template.


Editor grafico: Definizione del Sistema

System declaration: contiene la dichiarazione dei processi che compongono il sistema. (system Train, Gate)

Fig.8 Dichiarazione componenti sistema.

Fig.8 Dichiarazione componenti sistema.


Esempio di specifica

Il seguente esempio di specifica è fornito dalla distribuzione UPPAAL insieme al sistema e può dunque essere esaminato in dettaglio.

Problema: si vuole definire un sistema di controllo ferroviario per la gestione dell’accesso di più treni, ad un singolo ponte.
Il ponte è la risorsa critica condivisa, poiché solo un treno alla volta può occupare il ponte (nell’esempio sono previsti 4 treni).

Requisiti del problema
Un treno non può fermarsi, e nemmeno ripartire, in modo istantaneo (operazioni con durata non nulla).
Quando un treno si approssima al ponte invia il segnale Appr! per manifestare l’intenzione di occuparlo.
Dall’avvio del segnale appr! vi sono 10 unità di tempo per ricevere un eventuale segnale di stop (tempo necessario al treno per fermarsi in sicurezza).
Dopo queste 10 unità di tempo, il treno impiega altre 10 unità prima di salire sul ponte.
Se un treno è stato fermato, esso riparte quando il controller invia il segnale Go!
Quando il treno che ha occupato il ponte lo libera invia al controller il segnale leave!
Il controllo gestisce le richieste di accesso al ponte con politica FIFO.

Template per il treno e per il controller del ponte


Commenti template per il treno

La definizione parametrica del treno (uso del parametro [id]) consentirà l’istanziazione di quattro istanze di treno.

La locazione iniziale del treno Safe indica che il treno non è in fase di approccio al ponte. Lo stato non ha inviarianti e ciò implica che il treno può essere in tale locazione per un periodo indefinito di tempo.

Quando il treno è in fase di salita si sincronizza col controller usando il canale in uscita appr! sulla transizione che porta ad Appr (il controller ha una corrispondente azione Appr?).

L’orologio x viene azzerato e la variabile e viene settata per identificare il treno.

La locazione Appr ha l’invariante x  \leq 20, e quindi deve essere abbandonata entro 20 unità di tempo.

Le due transizioni uscenti da Appr hanno come guardia i vincoli x \leq 10<br /> \mbox{ e } x  \geq 10 per gestire le situazioni in cui il treno è fermato o non fermato.

Commenti template per il treno (segue)

Se il treno può essere fermato x \leq  10, allora può essere presa la transizione che porta a Stop con guardia e == id e sincronizzata con stop?.
(il controller decide di fermare un treno assegnando alla variabile e il valore opportuno).

La locazione Stop non ha inviarianti: un treno può essere fermato per una quantità illimitata di tempo.

Un treno fermo aspetta di sincronizzarsi con go?. La guardia e == id assicura che il treno corretto riparta (se più d’uno è in attesa).

La locazione Start ha l’invariante x \leq 15 e la transizione in uscita ha la guardia x \geq 7: quando il treno riparte raggiunge il ponte in un tempo compreso fra 7 e 15 unità di tempo.

La locazione Cross è abbandonata fra 3 e 5 unità di tempo (durata attraversamento).

Commenti template per il controller del ponte

Se la coda di attesa è vuota (len == 0) allora il controller aspetta l’approccio del treno, tramite la sincronizzazione appr?.

Quando un treno invia appr!, è aggiunto alla coda e il controller va nella locazione Occ.

Se la coda non è vuota, allora il primo treno della coda è autorizzato a percorrere il ponte (sincronizzazione Go!).

Nella locazione Occ, il controller aspetta che un treno comunichi l’attraversamento del ponte (sincronizzazione leave?).

In Occ, un altro treno potrebbe inviare il segnale di avvicinamento: in tal caso una transizione porta nella Committed Location, mettendo in coda il treno.

Per la priorità delle Committed Location, non può esserci ritardo nell’invio del segnale di arresto al treno.

Commenti template per il controller del ponte (segue)

E’ possibile estendere l’insieme dei metodi definiti sui tipi di dati definiti nei template.

Le operazioni definite possono comparire nell’azione di una transizione.

Esempio: si vedano le operazioni di

  • Enqueue(…)
  • Dequeue(…)

Per aggiungere e rimuovere l’identificatore di un treno nell’array che implementa una coda.

Fig.9 Azioni definibili da utente.

Fig.9 Azioni definibili da utente.


  • Contenuti protetti da Creative Commons
  • Feed RSS
  • Condividi su FriendFeed
  • Condividi su Facebook
  • Segnala su Twitter
  • Condividi su LinkedIn
Progetto "Campus Virtuale" dell'Università degli Studi di Napoli Federico II, realizzato con il cofinanziamento dell'Unione europea. Asse V - Società dell'informazione - Obiettivo Operativo 5.1 e-Government ed e-Inclusion