The bounded retransmission protocol must be on time!
D'Argenio, P.R. and Katoen, J.P. and Ruys, T.C. and Tretmans, G.J. (1997) The bounded retransmission protocol must be on time! In: Proceedings of the Third Workshop on Tools and Algorithms for the Construction and Analysis of Systems.
Restricted to UT campus only: Request a copy
|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.|
Supported by the NWO/SION project 612-33-006.
|Item Type:||Conference or Workshop Item|
Electrical Engineering, Mathematics and Computer Science (EEMCS)
|Link to this item:||http://purl.utwente.nl/publications/63292|
|Export this item as:||BibTeX|
Daily downloads in the past month
Monthly downloads in the past 12 months
Repository Staff Only: item control page