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
Un ascensore autonomo opera fra due piani Piano 0 e Piano 1.
Il comportamento dell’ascensore rispetta i seguenti requisiti:
La proposta di specifica prevede la definizione di tre template:
Il sistema è costituito dalla composizione parallela di:
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.
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
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?.
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.
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?.
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
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
La variante contempla la possibilità di prenotazione (chiamata) dell’ascensore.
La specifica consiste di tre template.
Persona: descrive il comportamento di una singola persona.
Ascensore: descrive 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:
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.
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.
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!
Il template Controller gestisce le prenotazionialla ricezione di pressOpen! riapre le porte sincronizzandosi con l’ascensore tramite Open!:
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.
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