Modeling and verifying a bounded retransmission protocol
| Title | Modeling and verifying a bounded retransmission protocol |
| Publication Type | Conference Paper |
| Year of Publication | 1996 |
| Authors | D'Argenio, PR, Katoen, J-P, Ruys, TC, Tretmans, J |
| Editor | Brezocnik, Z, Kapus, T |
| Conference Name | Proc. of COST 247 International Workshop on Applied Formal Methods in System Design, {\rm Maribor, Slovenia} |
| Publisher | University of Maribor |
| 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 retransmission of a frame, 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. A comparison between these approaches is made and our experiences are reported. (Succeeded by TACAS 1996, LNCS 1217, pp. 416-431, Springer.) |
PDF (Full text):
