181 lines
8 KiB
Org Mode
181 lines
8 KiB
Org Mode
|
* 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/.
|
|||
|
|
# \includepdf{sender_A.jpg}
|
|||
|
|
[[./sender_A.jpg]]
|
|||
|
|
** 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/.
|
|||
|
|
[[./receiver_A.jpg]]
|
|||
|
|
** 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].
|
|||
|
|
[[./link_A.jpg]]
|
|||
|
|
** 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/
|
|||
|
|
[[./link_B.jpg]]
|
|||
|
|
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/.
|
|||
|
|
[[./trace_B.jpg]]
|
|||
|
|
\includepdf{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.waitACK –> (sender.receivedACK)
|
|||
|
|
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.
|
|||
|
|
[[./receiver_C.jpg]]
|
|||
|
|
** 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.
|
|||
|
|
[[./sender_2t.jpg]]
|
|||
|
|
[[./sender_1t.jpg]]
|
|||
|
|
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_pkg -> resend_pkg = 4
|
|||
|
|
Receiver: recv_pkg -> done_pkg = 4
|
|||
|
|
Receiver: done_pkg -> send_ack = 4
|
|||
|
|
Link: received_ack -> resend_ack = 4
|
|||
|
|
|
|||
|
|
# Perdita per receiver
|
|||
|
|
Link: received_pkg -> resend_pkg = 4
|
|||
|
|
Receiver: recv_pkg -> is_dup = 4
|
|||
|
|
Receiver: is_dup -> send_ack = 4
|
|||
|
|
Link: received_ack -> resend_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.
|