The Bounded Retransmission Protocol must be on time!

P.R. d' Argenio, Joost P. Katoen, T.C. Ruys, G.J. Tretmans

Research output: Book/Report › Report › Professional

50 Citations (Scopus)
48 Downloads (Pure)

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.
Original languageUndefined
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
Number of pages63
Publication statusPublished - 1997

Publication series

NameCTIT technical report
PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
No.97-03

Keywords

  • IR-18600
  • METIS-119121
  • EWI-6034

Cite this

d' Argenio, P. R., Katoen, J. P., Ruys, T. C., & Tretmans, G. J. (1997). The Bounded Retransmission Protocol must be on time! (CTIT technical report; No. 97-03). Enschede: Centre for Telematics and Information Technology (CTIT).
d' Argenio, P.R. ; Katoen, Joost P. ; Ruys, T.C. ; Tretmans, G.J. / The Bounded Retransmission Protocol must be on time!. Enschede : Centre for Telematics and Information Technology (CTIT), 1997. 63 p. (CTIT technical report; 97-03).
@book{ced21e1eb87c4739a71364e7119fee3d,
title = "The Bounded Retransmission Protocol must be on time!",
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.",
keywords = "IR-18600, METIS-119121, EWI-6034",
author = "{d' Argenio}, P.R. and Katoen, {Joost P.} and T.C. Ruys and G.J. Tretmans",
note = "Imported from CTIT",
year = "1997",
language = "Undefined",
series = "CTIT technical report",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "97-03",
address = "Netherlands",

}

d' Argenio, PR, Katoen, JP, Ruys, TC & Tretmans, GJ 1997, The Bounded Retransmission Protocol must be on time! CTIT technical report, no. 97-03, Centre for Telematics and Information Technology (CTIT), Enschede.

The Bounded Retransmission Protocol must be on time! / d' Argenio, P.R.; Katoen, Joost P.; Ruys, T.C.; Tretmans, G.J.

Enschede : Centre for Telematics and Information Technology (CTIT), 1997. 63 p. (CTIT technical report; No. 97-03).

Research output: Book/Report › Report › Professional

TY - BOOK

T1 - The Bounded Retransmission Protocol must be on time!

AU - d' Argenio, P.R.

AU - Katoen, Joost P.

AU - Ruys, T.C.

AU - Tretmans, G.J.

N1 - Imported from CTIT

PY - 1997

Y1 - 1997

N2 - 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.

AB - 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.

KW - IR-18600

KW - METIS-119121

KW - EWI-6034

M3 - Report

T3 - CTIT technical report

BT - The Bounded Retransmission Protocol must be on time!

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

d' Argenio PR, Katoen JP, Ruys TC, Tretmans GJ. The Bounded Retransmission Protocol must be on time! Enschede: Centre for Telematics and Information Technology (CTIT), 1997. 63 p. (CTIT technical report; 97-03).

Access to Document