Abstract
This paper concerns the transfer of files via a lossy communication channel. It formally specifies this file transfer service in a property-oriented way and investigates -using two different techniques -whether a given bounded retransmission protocol conforms to this service. This protocol is based on the well-known alternating bit protocol but allows for a bounded number of retransmissions of a chunk, i.e., part of a file, only. So, eventual delivery is not guaranteed and the protocol may abort the file transfer. We investigate to what extent real-time aspects are important to guarantee the protocol's correctness and use Spin and Uppaal model checking for our purpose.
| Original language | Undefined |
|---|---|
| Place of Publication | Enschede |
| Publisher | Centre for Telematics and Information Technology (CTIT) |
| Number of pages | 63 |
| Publication status | Published - 1997 |
Publication series
| Name | CTIT technical report |
|---|---|
| Publisher | University of Twente, Centre for Telematics and Information Technology (CTIT) |
| No. | 97-03 |
Keywords
- IR-18600
- METIS-119121
- EWI-6034
Cite this
d' Argenio, P. R., Katoen, J. P., Ruys, T. C., & Tretmans, G. J. (1997). The Bounded Retransmission Protocol must be on time! (CTIT technical report; No. 97-03). Enschede: Centre for Telematics and Information Technology (CTIT).