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.
|Place of Publication||Enschede|
|Publisher||Centre for Telematics and Information Technology (CTIT)|
|Number of pages||63|
|Publication status||Published - 1997|
|Name||CTIT technical report|
|Publisher||University of Twente, Centre for Telematics and Information Technology (CTIT)|
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).