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
 
I corsi di Scienze Matematiche Fisiche e Naturali
 
Il Corso Le lezioni del Corso La Cattedra
 
Materiali di approfondimento Risorse Web Il Podcast di questa lezione

Adriano Peron » 20.Esercizio di specifica in UPPAAL


Temi della lezione

Nella lezione viene presentato un esercizio di specifica in UPPAAL assegnato agli studenti e viene riportata la soluzione all’esercizio proposta da uno studente (senza le eventuali osservazioni/correzioni del docente).

Il lettore è invitato a valutare criticamente le scelte adottate.

Contenuto

  • Requisiti del problema.
  • Specifica.
  • Proprietà.
  • Variante della specifica.

Ascensore: Requisiti

Un ascensore autonomo opera fra due piani Piano 0 e Piano 1.

Il comportamento dell’ascensore rispetta i seguenti requisiti:

  • quando l’ascensore arriva ad piani si ferma e, dopo 2 secondi, le porte cominciano ad aprirsi automaticamente e completano l’apertura entro 5 secondi;
  • le persone possono entrare o uscire solo quando le porte sono completamente aperte;
  • solo una persona alla volta può varcare le porte in ingresso/uscita (si assume che la capienza dell’ascensore consenta di servire servire il numero di persone in attesa);
  • una persona decide in modo non deterministico se usare l’ascensore;
  • una persona salita sull’ascensore può solo decidere di scendere;
  • le porte si chiudono automaticamente dopo 4 secondi dall’ingresso dell’ultima persona;
  • alla chiusura delle porte trascorrono 2 secondi prima che l’ascensore parta;
  • la durata della percorrenza di un piano è 20 secondi.

Proposta di specifica 1

La proposta di specifica prevede la definizione di tre template:

  1. Persona: descrive il comportamento di una singola persona;
  2. Ascensore: descrive il comportamento del controllore dell’ascensore;
  3. Mutex: È una componente che controlla che l’accesso alle porte in ingresso/uscita sia fatto da una sola persona.

Il sistema è costituito dalla composizione parallela di:

  • N processi che istanziano il template Persona (N=5 nell’attività di verifica);
  • un processo che istanzia il template Ascensore;
  • un processo che istanzia il template Mutex.

Template persona


Template persona: Commenti

La locazione iniziale Init, inizializza la variabile p locale ad ogni processo; p memorizza il piano su cui si trova la persona nei diversi istanti di tempo. La locazione è committed per evitare che l’inizializzazione sia rimandata nel tempo.

La locazione Idle indica che la persona non desidera utilizzare l’ascensore; la persona può rimanere a tempo indefinito nella locazione non essendoci invariante.

Una persona può decidere di salire sull’ascensore passando dalla Locazione Idle alla locazione WillToEnter (la transizione non ha guardia).

Una persona può decidere di scendere dall’ascensore in maniera non-deterministica transendo dalla locazione Travel alla locazione WillToExit.

Una persona può salire solo se si trova allo stesso piano dell’ascensore.

Per salire o scendere serve sincronizzarsi con il processo Mutex inviando il segnale enter [id]? (risp.exit [id]?).

La locazione ReadyToEnter, rispettivamente Ready-ToExit, ha un’invariante x<= 2 e di conseguenza deve essere abbandonata entro 2 unità di tempo.

Template persona: Commenti (segue)

La transizione uscente da ReadyToEnter etichettata con wait [id]? permette al Mutex di mettere la persona in attesa del suo turno di salita.

Una persona messa in attesa, aspetta (un tempo arbitrario) per sincronizzarsi con proceed [id]? per procedere ad entrare, se si trova in WaitToEnter, o rispettivamente uscire, se in WaitToExit.

La persona si sincronizza con il Mutex attraverso il canale done per segnalare che è entrata, rispettivamente uscita dall’ascensore.

Per evitare ritardi immotivati per entrare o uscire i canali enter, exit, proceed e done sono dichiarati urgenti.

Per evitare che una persona entri ed esca in continuazione bloccando l’ascensore

  • ad un piano si usa il canale broadcast go;
  • se una persona è già salita nell’ascensore per transire alla locazione da cui può decidere di scendere WillToExit deve prima sincronizzarsi su go?. La sincronizzazione può avvenire solo durante la chiusura delle porte impedendo alla persona di scendere subito.

Template Ascensore


Template Ascensore: Commenti

L’ascensore sale e scende continuamente tra i due piani (non è prevista la chiamata con prenotazione che può far scendere e salire l’ascensore vuoto).

La locazione iniziale Init è utilizzata per inizializzare la variabile piano che indica il piano su cui si trova l’ascensore nei diversi istanti di tempo. L’ascensore dispone di un clock x, che usa per imporre i vincoli temporali sulle transizioni.

La locazione Stillindica che l’ascensore è appena arrivato in uno dei due piani. Per la presenza dell’invariante x <= 2 e la guardia sull’unica transizione uscente implica che ogni volta che l’ascensore arriva nella locazione, dopo esattamente 2 unità di tempo deve abbandonarla transendo verso la locazione Opening.

Entro 5 secondi le porte si aprono completamente, e quindi l’ascensore transita da Opening verso la locazione Open. La transizione si sincronizza con free! e assicura che solo da quell’istante le persone possano entrare o uscire.

Durante la transizione viene aggiornata la variabile piano per riflettere il piano su cui si trova l’ascensore.

Per chiudere le porte l’ascensore aspetta di sincronizzarsi con go?.

Template Mutex


Template Mutex: Commenti

Il processo Mutex è sincronizzato con il processo Ascensore ed implementa la mutua esclusione nell’accesso all’ascensore mettendo in coda le persone che vogliono entrare o uscire permettendolo ad una sola persona alla volta.

L’unica transizione uscente da Move si sincronizza con free! dell’ascensore per assicurare che la transizione verso Free avvenga solo a porte aperte.

Nella locazione Free il mutex è abilitato di ricevere richieste dalle persone.

Se la coda è vuota il mutex aspetta che una persona chieda di salire tramite la sincronizzazione enter [id]? o rispettivamente di scendere tramite la sincronizzazione exit [id]?.

Quando una persona invia enter [id]? o exit [id]?, viene aggiunta alla coda e il mutex si sposta nella locazione Occ.

Se la coda non è vuota, alla prima persona nella coda viene inviato proceed [id]! Perché proceda a entrare o uscire dall’ascensore.

Template Mutex: Commenti (segue)

Per ritornare nella locazione Free il mutex deve aspettare che la persona che sta entrando o uscendo invii done [id]!.

Nella locazione Occ il mutex può ricevere richieste da persone che vogliono entrare o uscire. Le transizioni portano ad una Committed Location mettendole in coda.

Dalla locazione Committed il mutex deve subito ritornare in Occ in quanto non può esserci attesa, mettendo cosi in attesa l’ultima persona tramite la sincronizzazione sul canale wait.

Ogni volta che una persona entra od esce il clock del mutex viene risettato. Se entro 4 unità di tempo non viene ricevuta nessuna richiesta il mutex si sincronizza con l’ascensore tramite go?.

Verifica di proprietà

Esempi di proprietà soddisfatte dal sistema (verificato con 5 istanze di persona).

La Persona 0 può entrare nell’ascensore mentre tutte le altre persone stanno aspettando di entrare.

E<> Persona(0).Entering and (forall (i : id_p) i != 0 imply Persona(i).WaitToEnter)

Due diverse persone non possono mai entrare o uscire contemporaneamente nell’ascensore.

A[] forall (i : id_p) forall (j : id_p) Persona(i).Entering && Persona(j).Entering imply i == j

A[] forall (i : id_p) forall (j : id_p) Persona(i).Exiting && Persona(j).Exiting imply i == j

Non possono mai esserci N+1 persone in coda.
A[] Mutex.len <=N

Verifica di proprietà (segue)

Il tempo che una persona può impiegare per entrare nell’ascensore è limitato da 2*(2+20+5) + 2*(N-1)*(4+2)+4.

A[] forall (i : id_p) Persona(i).WillToEnter imply Persona(i).x

Il tempo che una persona può impiegare per uscire dall’ascensore è limitato da (2+20+5).

A[] forall (i : id_p) Persona(i).WillToExit imply Persona(i).x

Una persona in attesa per entrare nell’ascensore (o uscire), appena possibile entrerà.

Persona(0).WillToEnter --> Persona(0).In

Persona(0).WillToExit --> Persona(0).Exiting

Non si possono mai verificare deadlock nel sistema.

A[] not deadlock

Variante della specifica

La variante contempla la possibilità di prenotazione (chiamata) dell’ascensore.

La specifica consiste di tre template.

Persona: descrive il comportamento di una singola persona.

Ascensoredescrive il comportamento del controllore dell’ascensore.

Controller: Gestisce l’apetto della chiamata dell’ascensore.

Mutex: Il mutex viene omesso per semplicità e la sua funzionalità di mutua esclusione per l’ingresso uscita viene gestita in modo più basico (senza coda).

Il sistema è costituito dalla composizione parallela di:

  • N processi che istanziano il template Persona (N=5 nell’attività di verifica);
  • un processo che istanzia il template Ascensore;
  • un processo che istanzia il template Controller.

Template Persona-b


Template persona: Commenti

La mutua esclusione nell’accesso dell’ascensore è garantita dall’uso dei canali enter e exit. Per entrare o uscire una persona deve sincronizzarsi con l’ascensore inviando enter? o exit?.

Se trovandosi nello stato Will-ToEnter la persona non trova le porte dell’ascensore aperte sullo stesso piano, può effettuare una chiamata inviando call! e assegnare alla variabile cbotton il numero di piano su cui si trova.

Il controllore si sincronizza con call? e memorizza la chiamata aggiornando l’array calls usato per registrare le chiamate non ancora servite.

La persona resta nella locazione WaitToEnter fino all’apertura delle porte dell’ascensore sul suo piano che la fa ritornare nella locazione WillToEnter dove rimane in attesa per sincronizzarsi sul canale enter.

Non appena le porte si chiudono la persona preme il tasto all’interno dell’ascensore per farlo andare al piano desiderato inviando pressButton! al controllore che invierà il segnale go! all’ascensore.

Template persona: Commenti (segue)

Ogni persona che si trova nell’ascensore può non deterministicamente decidere quando scendere passando alla locazione WillToExit.

Se l’ascensore si trova fermo su uno dei piani con le porte chiuse la persona può premere il tasto all’interno dell’ascensore per forzare l’apertura delle porte inviando pressOpen! al controllore che avrà il compito di sincronizzarsi con l’ascensore per fargli aprire le porte tramite open!.

In caso contrario la persona aspetta per sincronizzarsi con l’ascensore sul canale exit.

Template Ascensore-b


Template Ascensore

Il template è sostanzialmente analogo a quello della prima versione. Si evidenziano solo le seguenti differenze che hanno lo scopo di implementare la funzionalità di prenotazione.

La possibilità di far riaprire le porte dell’ascensore implementata tramite una nuova transizione che si sincronizza sul canale urgente open.

Se nessuno vuole usarlo, l’ascensore rimane fermo con le porte chiuse su un piano. L’ascensore parte solo se riceve go? da parte del controllore, ovvero nei casi in cui sono entrate una o più persona o c’è stata una chiamata dall’altro piano.

Entro 2 unità di tempo dal momento in cui l’ascensore va nella locazione Closed viene effettuato un controllo delle prenotazioni attraverso l’invio di check!

Template Controller-b


Template Controller

Il template Controller gestisce le prenotazionialla ricezione di pressOpen! riapre le porte sincronizzandosi con l’ascensore tramite Open!:

  • alla ricezione di pressButton! far partire l’ascensore inviandogli go!
  • alla ricezione di check! verifica se vi sono chiamate non servite e:
    • invia open! se vi è una prenotazione dal piano in cui si trova;
    • invia open! se vi è una prenotazione dal piano in cui si trova;
    • inviare go! se la prenotazione proviene da altro piano.

In presenza di più prenotazioni viene fatta una scelta non deterministica su quale servire.

Per dare una precedenza a una delle due è possibile dichiarare la priorità dei canali open e go (bisogna tener presente che UPPAAL non sarebbe più in grado di verificare la presenza di deadlock nel sistema).

Alla ricezione di doorOpen! azzerare le prenotazioni per il piano di arrivo.

  • 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