200 lines
9 KiB
Org Mode
Executable file
200 lines
9 KiB
Org Mode
Executable file
#+TITLE: Esercizio Timed Automata
|
|
#+AUTHOR: Francesco Mecca
|
|
#+EMAIL: me@francescomecca.eu
|
|
#+LANGUAGE: en
|
|
#+LaTeX_CLASS: article
|
|
#+LaTeX_HEADER: \linespread{1.25}
|
|
#+LaTeX_HEADER: \usepackage{pdfpages}
|
|
#+LaTeX_HEADER: \usepackage{comment}
|
|
|
|
#+EXPORT_SELECT_TAGS: export
|
|
#+EXPORT_EXCLUDE_TAGS: noexport
|
|
#+OPTIONS: H:2 toc:nil \n:nil @:t ::t |:t ^:{} _:{} *:t TeX:t LaTeX:t
|
|
#+STARTUP: showall
|
|
* 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\under{}pkg/ che invia il pacchetto sul canale di
|
|
sincronizzazione urgente /ML/. Il sender passa allo stato /wait\under{}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/.
|
|
#+CAPTION: Sender protocollo A
|
|
[[./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\under{}pkg/, simulando la preparazione del
|
|
pacchetto in un intervallo di tempo [2;4].
|
|
La transizione dallo stato /done\under{}pkg/ a /send\under{}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/.
|
|
#+CAPTION: Receiver protocollo A
|
|
[[./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\under{}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\under{}ack/ dal canale di trasmissione
|
|
/RL/ e l'invio verso il sender dallo stato /resend\under{}ack/ attraverso il
|
|
canale di trasmissione /LM/. Per il processing dei pacchetti
|
|
l'intervallo di tempo e` sempre [2;4].
|
|
#+CAPTION: Link protocollo A
|
|
[[./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\under{}ack
|
|
| A<> sender.received\under{}ack
|
|
la proprieta` risulta vera in quanto il link non ha perdite.
|
|
- Il receiver ricevera` sempre un pacchetto
|
|
| AF receiver.recv\under{}pkg
|
|
| A<> receiver.recv\under{}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\under{}pkg/ e /received\under{}ack/ verso
|
|
/loss/
|
|
#+CAPTION: Link protocollo B
|
|
[[./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\under{}ack/ → /loss/.
|
|
#+CAPTION: Trace con deadlock
|
|
[[./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.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\under{}pkg
|
|
| A<> receiver.recv\under{}pkg
|
|
che come per la proprieta` precedente non puo` risultare vera
|
|
- Il receiver puo` ricevere un pacchetto
|
|
| EF receiver.recv\under{}pkg
|
|
| E<> receiver.recv\under{}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\under{}frame/ per tenere
|
|
traccia degli pacchetti gia` ricevuti e processati.
|
|
#+CAPTION: Receiver protocollo C
|
|
[[./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\under{}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.
|
|
#+CAPTION: Sender protocollo C (due timer)
|
|
[[./sender_2t_C.jpg]]
|
|
#+CAPTION: Sender protocollo C (un timer)
|
|
[[./sender_1t_C.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\under{}dup/ e /done\under{}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\under{}pkg \vert{}\vert{} sender.send\under{}pkg1 \vert{}\vert{} receiver.send\under{}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\under{}pkg \vert{}\vert{} receiver.send\under{}ack)
|
|
la proprieta` e` rispettata
|
|
- Il receiver ricevera` sempre un pacchetto
|
|
| sender.wait\under{}ack \vert{}\vert{} sender.wait\under{}ack1 --> (sender.received\under{}ack \vert{}\vert{} sender.received\under{}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.
|