The bounded retransmission protocol must be on time!

Hendrik Brinksma (Editor), P.R. d' Argenio, Joost P. Katoen, T.C. Ruys, G.J. Tretmans

Research output: Contribution to conferencePaperAcademicpeer-review

28 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. Supported by the NWO/SION project 612-33-006.
Original languageUndefined
Pages416-431
Number of pages16
DOIs
Publication statusPublished - 1997

Keywords

  • FMT-MC: MODEL CHECKING
  • EWI-6470
  • FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
  • IR-63292

Cite this

@conference{c3c0082ec9ed42c5975e0f20958156b0,
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. Supported by the NWO/SION project 612-33-006.",
keywords = "FMT-MC: MODEL CHECKING, EWI-6470, FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS, IR-63292",
author = "Hendrik Brinksma and {d' Argenio}, P.R. and Katoen, {Joost P.} and T.C. Ruys and G.J. Tretmans",
year = "1997",
doi = "10.1007/BFb0035403",
language = "Undefined",
pages = "416--431",

}

The bounded retransmission protocol must be on time! / Brinksma, Hendrik (Editor); d' Argenio, P.R.; Katoen, Joost P.; Ruys, T.C.; Tretmans, G.J.

1997. 416-431.

Research output: Contribution to conferencePaperAcademicpeer-review

TY - CONF

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.

A2 - Brinksma, Hendrik

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. Supported by the NWO/SION project 612-33-006.

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. Supported by the NWO/SION project 612-33-006.

KW - FMT-MC: MODEL CHECKING

KW - EWI-6470

KW - FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS

KW - IR-63292

U2 - 10.1007/BFb0035403

DO - 10.1007/BFb0035403

M3 - Paper

SP - 416

EP - 431

ER -