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. Supported by the NWO/SION project 612-33-006.
|Number of pages||16|
|Publication status||Published - 1997|
- FMT-MC: MODEL CHECKING
- FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS