Introduzione alla verifica di sistemi real-time in UPPAL:
Estensione degli automi temporizzati con le seguenti caratteristiche.
Composizione parallela di automi temporizzati (Rete di Timed automata).
Canali di comunicazione tra componenti parallele:
Uso di variabili condivise:
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:
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.
.
La semantica delle reti di automi estende naturalmente al caso parallelo la semantica degli automi temporizzati:
La semantica della rete XTA di automi temporizzati viene data definendo un LTS
Lo stato raccoglie informazioni sul controllo di tutte le componenti e sulla valutazione corrente degli orologi (comune a tutte le componenti).
Gli stati iniziali hanno valutazione dei clock a tempo zero.
con
L’insieme di transizioni è l’unione dei tre seguenti insiemi di transizioni.
1) Il tempo avanza di un quantità t uniformemente per tutte le componenti:
(2) Una componente fa una mossa interna asincrona
(2) Due componenti fanno una mossa sincrona di comunicazione
Sono possibili tre tipi distinti di locazioni:
(1) Locazioni normali
(2) Locazioni urgenti
Esempio
Le transizioni debbono scattare simultaneamente in un istante
Dopo il loro scatto non vi può essere avanzamento temporale perché lo stato contiene una componente urgente.
La transizione deve eseguita al tempo t.
La transizione può essere eseguita nell’intervallo [t,2].
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 scatti per prima seguita dalla sincronizzazione di .
hanno la priorità su
Le sequenze possibili sono:
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.
Contine la dichiarazione di elementi globali:
Templates: contiene la dichiarazione degli Automi Temporizzati parametrizzati. Un template può avere dichiarazioni locali di variabili, canali e costanti.
System declaration: contiene la dichiarazione dei processi che compongono il sistema. (system Train, Gate)
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.
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 , e quindi deve essere abbandonata entro 20 unità di tempo.
Le due transizioni uscenti da Appr hanno come guardia i vincoli per gestire le situazioni in cui il treno è fermato o non fermato.
Se il treno può essere fermato , 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 e la transizione in uscita ha la guardia : 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).
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.
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
Per aggiungere e rimuovere l’identificatore di un treno nell’array che implementa una coda.
1. Introduzione ai metodi formali di specifica
2. Semantica dei formalismi di specifica
3. Astrazione e Bisimulazione debole
4. FSM: Macchine a Stati Finiti
5. FSM: Non-determinismo e succintezza
7. FSM e Parallelismo – seconda parte
8. FSM e Parallelismo – terza parte
9. Promela
10. Specifica e verifica in SPIN
11. Proprietà di liveness in SPIN
12. Specifica di proprietà in Logica Temporale Lineare
13. Comportamenti infiniti: Automi di Büchi
14. Model checking di LTL basato su automi
15. Specifica di sistemi real time: Automi Temporizzati
16. Proprietà degli Automi Temporizzati
17. Problemi di decisione negli Automi Temporizzati
18. Il sistema di verifica UPPAAL