next up previous

Final Report of the COST-247 Action


Pedro R. D'Argenio, Joost-Pieter Katoen, Theo Ruys, and Jan Tretmans

Tele-Informatics and Open Systems Group
Department of Computer Science
University of Twente
P.O. Box 217
7500 AE Enschede, The Netherlands
E-mail: , , ,
tel: +31 53 489 4287
fax: +31 53 489 3247


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 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 {\sc Spin} and {\sc Uppaal} model checking for our purpose. A comparison between these approaches is made and our experiences are reported.

This presentation has been given during the COST-247 International Workshop on Applied Formal Methods in System Design (Maribor, Slovenia, June 17--19, 1996).

COST-247 Working Group(s): 2

This Page was prepared by Mark Jorgensen.

Back to the VASY Home page