The Bounded Retransmission Protocol Must Be on Time!
Title | The Bounded Retransmission Protocol Must Be on Time! |
Publication Type | Conference Paper |
Year of Publication | 1997 |
Authors | D'Argenio, PR, Katoen, J-P, Ruys, TC, Tretmans, J |
Editor | Brinksma, E |
Conference Name | Tools and Algorithms for Construction and Analysis of Systems, Third International Workshop, TACAS '97, Enschede, The Netherlands, April 2-4, 1997, Proceedings |
Publisher | Springer |
ISBN Number | 3-540-62790-1 |
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. |
DOI | 10.1007/BFb0035403 |
PDF (Full text):