9 KiB
Esercizio Timed Automata
Modello A
Sono stati usati tre template per rappresentare un sender, un link wd un receiver
| sender = Sender(); |
| receiver = Receiver(); |
| link = Link(); |
| system sender, receiver, link; |
Sender
Lo stato iniziale dell'automata e` wait che simula l'attesa dell'arrivo di un pacchetto che viene processato nell'intervallo [1;2] del clock sc. Lo stato successivo e` send_pkg che invia il pacchetto sul canale di sincronizzazione urgente ML. Il sender passa allo stato wait_ack che simula l'attesa di un pacchetto sul canale di sincronizzazione urgente LM e resetta il clock sc. Viene simulata la verifica dell'ack in un intervallo di tempo [2;4] e successivamente l'automa torna allo stato iniziale resettando il clock sc.
Receiver
Il receiver e` simmetrico al sender. Dallo stato iniziale di wait viene simulato l'arrivo di un pacchetto sul canale di sincronizzazione urgente LR che permette al receiver di resettare il clock rc e avanzare nello stato recv_pkg, simulando la preparazione del pacchetto in un intervallo di tempo [2;4]. La transizione dallo stato done_pkg a send_ack simula la generazione di un pacchetto di ack in un intervallo di tempo [2;4] ed tornare allo stato iniziale dopo aver inviato il pacchetto nel canale di sincronizzazione urgente RL.
Link
Il link e` modellato come un canale perfetto senza perdite. Lo stato interno idle simula l'attesa di un pacchetto da parte del receiver o del sender. Lo stato received_pkg simula l'arrivo di un pacchetto da parte del sender sul canale ML che viene processato e spedito al receiver sul canale LR. Simmetricamente le stesse operazioni di attesa, processing e invio avvengono con i pacchetti di ack di cui si simula l'arrivo nello stato received_ack dal canale di trasmissione RL e l'invio verso il sender dallo stato resend_ack attraverso il canale di trasmissione LM. Per il processing dei pacchetti l'intervallo di tempo e` sempre [2;4].
Proprieta`
Sono state verificate tre proprieta` TCTL sul modello:
-
Assenza di deadlock
A[] (not deadlock) che viene rispettata e indica che la traccia del sistema e` infinita
-
Il sender ricevera` sempre un ack
AF sender.received_ack A<> sender.received_ack la proprieta` risulta vera in quanto il link non ha perdite.
-
Il receiver ricevera` sempre un pacchetto
AF receiver.recv_pkg A<> receiver.recv_pkg e` una proprieta` rispettata in quando non ci sono constraint sul tempo di attesa del pacchetto.
Tempo attesa
Il tempo di attesa viene calcolato attraverso il simulatore di Uppaal. E` stato inserito un clock che viene resettato ogni qualvolta viene inviato un pacchetto e una volta processato l'ack. L'intervallo di tempo che intercorre dall'invio del messaggio alla recezione del suo ack e` [11, 22).
Modello B
E` stato riutilizzato il sistema A e modificato il link per simulare la possibilita` di perdita o corruzione di un pacchetto.
Link
Come si denota dall'immagine il link e` simile a quello del modello A eccezion fatta per la possibilita` di procedere non deterministicamente dagli spazi received_pkg e received_ack verso loss
Mostriamo un trace in cui il link perde un pacchetto di ack inviato
dal sender e il sistema va in deadlock.
Dalla figura possiamo notare la transizione che simula la perdita,
ovvero l'arco received_ack → loss.
∈cludepdf{trace_B2.jpg}
Proprieta`
Sono state verificate quattro proprieta` TCTL sul modello:
-
Assenza di deadlock
A[] (not deadlock) che non e` rispettata
-
Il sender compiera` sempre del progresso
sender.wait_ack –> (sender.received_ack) la proprieta` non risulta vera in quanto il link ha perdite
-
Il receiver ricevera` sempre un pacchetto
AF receiver.recv_pkg A<> receiver.recv_pkg che come per la proprieta` precedente non puo` risultare vera
-
Il receiver puo` ricevere un pacchetto
EF receiver.recv_pkg E<> receiver.recv_pkg la proprieta` risulta vera perche` il link in alcuni path riesce ad inviare il pacchetto (non avvengono perdite sul canale)
Tempo attesa
Non si devono fare modifiche al modello rispetto al precedente per stabilire il tempo che intercorre dall'invio di un messaggio all'arrivo dell'ack. Bisogna pero` notare che in caso di deadlock l'ack non arriva mai al mittente e quindi effettivamente possiamo calcolare solo il tempo di ricezione minimo, ovvero 11 cicli del clock.
Modello C
E` stato riutilizzato il sistema B e modificati sender e receiver per simulare la possibilita` di recovery in seguito alla perdita o corruzione di uno o piu` pacchetti. Vengono anche mantenute due flag binarie globali, ack e frame per tenere traccia dei pacchetti inviati e degli ack ricevuti.
Receiver
Di seguito viene mostrato il receiver del modello C. Rispetto al Modello B il receiver utilizza una flag binaria locale r_frame per tenere traccia degli pacchetti gia` ricevuti e processati.
Sender
Il sender e` stato modellato raddopiando il numero di posti e archi, escludendo per lo stato iniziale, in modo da poter processare nella parte destra i frame di tipo 0 e nella parte sinistra i frame di tipo 1. Inoltre sono stati aggiunti due timer che, nel momento in cui l'automa e` fermo su wait_ack allo scadere del timeout, permettono di spostarsi nello spazio lost e riprovare l'invio del pacchetto. Si nota subito che i due timer sono indipendenti l'uno dall'altro e vi e` la possibilita` di modellare i sender senza duplicare il numero di spazi.
La variabile che regola il timeout e` un numero intero uguale o
maggiore del piu` grande fra i seguenti valore:
- il massimo tempo necessario all'invio di un pacchetto che il sender non ha processato
- il massimo tempo necessario all'invio di un pacchetto che il sender ha gia` processato
Se non si rispetta questo constraint il sistema va in deadlock. Nel modello utilizzato lo spazio is_dup e done_pkg del receiver hanno lo stesso invariante e il timeout TOUT ha valore minimo 16.
\begin{comment} Ho calcolato il timeout considerando i seguenti cammini # Perdita per sender Link: received\under{}pkg -> resend\under{}pkg = 4 Receiver: recv\under{}pkg -> done\under{}pkg = 4 Receiver: done\under{}pkg -> send\under{}ack = 4 Link: received\under{}ack -> resend\under{}ack = 4 # Perdita per receiver Link: received\under{}pkg -> resend\under{}pkg = 4 Receiver: recv\under{}pkg -> is\under{}dup = 4 Receiver: is\under{}dup -> send\under{}ack = 4 Link: received\under{}ack -> resend\under{}ack = 4 \end{comment}Proprieta`
Sono state verificate cinque proprieta` TCTL sul modello:
-
In caso di perdita il sender o il receiver tentano nuovamente di inviare il pacchetto
link.loss –> (sender.send_pkg || sender.send_pkg1 || receiver.send_ack) questa proprieta` e` rispttata.
-
Assenza di deadlock
A[] (not deadlock) questa proprieta` e` rispettata.
-
Nonostante una perdita nel link, il sender o il receiver riceveranno il pacchetto
link.loss –> (sender.send_pkg || receiver.send_ack) la proprieta` e` rispettata
-
Il receiver ricevera` sempre un pacchetto
sender.wait_ack || sender.wait_ack1 –> (sender.received_ack || sender.received_ack1) questa proprieta` non risulta vera dato che ci possono essere delle perdite nel canale
-
C'e` almeno un caso in cui l'ack ricevuto e` quello atteso
E<> (ack == expected) questa proprieta` risulta vera e conferma la correttezza del meccanismo di recovery loss.
Tempo attesa
In questo modello se si considera l'intervallo di tempo che intercorre dal primo tentativo di invio alla ricezione dell'ack, non e` possibile calcolare il valore massimo dell'intervallo. Questo perche` non e` possibile prevedere quanti tentativi saranno necessari per un corretto invio. Se invece si decide di resettare il clock ad ogni tentativo di invio, ovvero di calcolare l'intervallo di tempo che intercorre fra un pacchetto inviato in una situazione in cui il link non avra` perdite fino all'invio del relativo ack, allora si puo` considerare il modello equivalente al modello A, e quindi l'intervallo e` il medesimo.