Activities per year
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 language | English |
---|---|
Title of host publication | Tools and Algorithms for the Construction and Analysis of Systems |
Subtitle of host publication | Third International Workshop, TACAS'97, Enschede, The Netherlands, April 2-4, 1997, Proceedings |
Editors | Ed Brinksma |
Place of Publication | Berlin |
Publisher | Springer |
Pages | 416-431 |
Number of pages | 16 |
ISBN (Electronic) | 978-3-540-68519-7 |
ISBN (Print) | 978-3-540-62790-6 |
DOIs | |
Publication status | Published - 1997 |
Event | 3rd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1997 - University of Twente, Enschede, Netherlands Duration: 2 Apr 1997 → 4 Apr 1997 Conference number: 3 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 1217 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Workshop
Workshop | 3rd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1997 |
---|---|
Abbreviated title | TACAS |
Country/Territory | Netherlands |
City | Enschede |
Period | 2/04/97 → 4/04/97 |
Keywords
- FMT-MC: MODEL CHECKING
- FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
Fingerprint
Dive into the research topics of 'The bounded retransmission protocol must be on time!'. Together they form a unique fingerprint.Activities
- 1 Oral presentation
-
The Bounded Retransmission Protocol Must Be on Time!
Katoen, J.-P. (Invited speaker)
2 Apr 1997Activity: Talk or presentation › Oral presentation
Research output
- 1 Report
-
The Bounded Retransmission Protocol must be on time!
d' Argenio, P. R., Katoen, J.-P., Ruys, T. C. & Tretmans, G. J., 1997, Enschede: Centre for Telematics and Information Technology (CTIT). 63 p. (CTIT technical report; no. 97-03)Research output: Book/Report › Report › Professional
Open AccessFile