Modeling and Verifying a Bounded Retransmission Protocol

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

Modeling and Verifying a Bounded Retransmission Protocol

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

56 Downloads (Pure)

Abstract

This paper concerns the transfer of fies via a lossy communication channe. It formally specifies this file transfer service in a propert-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.

Original language	English
Title of host publication	Proceedings of COST 247 Workshop on Applied Formal Methods in System Design
Place of Publication	Maribor, Slovenia
Publisher	University of Maribor
Pages	114-127
Number of pages	15
ISBN (Print)	86-435-0155-7
Publication status	Published - 18 Nov 1996

Access to Document

ArticleFinal published version, 332 KB

http://lms.uni-mb.si/cost247/proc/

Modeling and Verifying a Bounded Retransmission Protocol
Tretmans, G. J., d' Argenio, P. R., Katoen, J.-P. & Ruys, T. C., 1996, Enschede: Centre for Telematics and Information Technology (CTIT). 14 p. (CTIT Technical Report Series; no. 96-22)
Research output: Book/Report › Report › Professional

Cite this

@inproceedings{b4718500bd724b0690e5edebfd225005,

title = "Modeling and Verifying a Bounded Retransmission Protocol",

abstract = "This paper concerns the transfer of fies via a lossy communication channe. It formally specifies this file transfer service in a propert-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.",

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

year = "1996",

month = nov,

day = "18",

language = "English",

isbn = "86-435-0155-7",

pages = "114--127",

booktitle = "Proceedings of COST 247 Workshop on Applied Formal Methods in System Design",

publisher = "University of Maribor",

address = "Slovenia",

}

TY - GEN

T1 - Modeling and Verifying a Bounded Retransmission Protocol

AU - d' Argenio, P.R.

AU - Katoen, J.-P.

AU - Tretmans, G.J.

AU - Ruys, T.C.

PY - 1996/11/18

Y1 - 1996/11/18

N2 - This paper concerns the transfer of fies via a lossy communication channe. It formally specifies this file transfer service in a propert-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.

AB - This paper concerns the transfer of fies via a lossy communication channe. It formally specifies this file transfer service in a propert-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.

M3 - Conference contribution

SN - 86-435-0155-7

SP - 114

EP - 127

BT - Proceedings of COST 247 Workshop on Applied Formal Methods in System Design

PB - University of Maribor

CY - Maribor, Slovenia

ER -

Modeling and Verifying a Bounded Retransmission Protocol

Abstract

Access to Document

Fingerprint

Research output

Modeling and Verifying a Bounded Retransmission Protocol

Cite this