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.

PDF
Restricted to UT campus only: Request a copy
314Kb

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
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/63292
Official URL:	http://dx.doi.org/10.1007/BFb0035403
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page