Formal verification of an improved sliding window protocol

D. Chkliaev, J.J.M. Hooman, E.P. Vink, de

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademic

54 Downloads (Pure)


The well-known Sliding Window protocol caters for the reliable and efficient transmission of data over unreliable channels that can lose, reorder and duplicate messages. Despite the practical importance of the protocol and its high potential for errors, it has never been formally verified for the general setting. We try to fill this gap by giving a fully formal specification and verification of an improved version of the protocol. The protocol is specified by a timed state machine in the language of the verification system PVS. This allows a mechanical check of the proof by the interactive proof checker of PVS. Our modelling is very general and includes such important features of the protocol as sending and receiving windows of arbitrary size, bounded sequence numbers and the three types of channel faults mentioned above.
Originele taal-2Engels
TitelProceedings 3rd PROGRESS Workshop on Embedded Systems (Utrecht, The Netherlands, October 24, 2002)
Plaats van productieUtrecht
UitgeverijSTW Technology Foundation
ISBN van geprinte versie90-73461-34-0
StatusGepubliceerd - 2002


Duik in de onderzoeksthema's van 'Formal verification of an improved sliding window protocol'. Samen vormen ze een unieke vingerafdruk.

Citeer dit