The Bounded Retransmission Protocol must be on time!

P.R. d' Argenio; J.-P. Katoen; T.C. Ruys; G.J. Tretmans

The Bounded Retransmission Protocol must be on time!

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

Research output: Book/Report › Report › Professional

65 Citations (Scopus)

100 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 language	English
Place of Publication	Enschede
Publisher	Centre for Telematics and Information Technology (CTIT)
Number of pages	63
Publication status	Published - 1997

Publication series

Name	CTIT technical report
Publisher	University of Twente, Centre for Telematics and Information Technology (CTIT)
No.	97-03

Access to Document

DArgenio1997boundedFinal published version, 655 KB

1 Oral presentation

The Bounded Retransmission Protocol Must Be on Time!
Katoen, J.-P. (Invited speaker)
2 Apr 1997
Activity: Talk or presentation › Oral presentation

65 Citations
1 Conference contribution

The bounded retransmission protocol must be on time!
d' Argenio, P. R., Katoen, J.-P., Ruys, T. C. & Tretmans, J., 1997, Tools and Algorithms for the Construction and Analysis of Systems: Third International Workshop, TACAS'97, Enschede, The Netherlands, April 2-4, 1997, Proceedings. Brinksma, E. (ed.). Berlin: Springer, p. 416-431 16 p. (Lecture Notes in Computer Science; vol. 1217).
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Open Access
File
44 Downloads (Pure)

Cite this

@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.",

author = "{d' Argenio}, P.R. and J.-P. Katoen and T.C. Ruys and G.J. Tretmans",

year = "1997",

language = "English",

series = "CTIT technical report",

publisher = "Centre for Telematics and Information Technology (CTIT)",

number = "97-03",

address = "Netherlands",

}

TY - BOOK

T1 - The Bounded Retransmission Protocol must be on time!

AU - d' Argenio, P.R.

AU - Katoen, J.-P.

AU - Ruys, T.C.

AU - Tretmans, G.J.

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.

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 -

The Bounded Retransmission Protocol must be on time!

Abstract

Publication series

Access to Document

Fingerprint

Activities

The Bounded Retransmission Protocol Must Be on Time!

Research output

The bounded retransmission protocol must be on time!

Cite this