University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Formal specification and verification of TCP extended with the Window Scale Option

Lockefeer, L, Williams, DM and Fokkink, W (2016) Formal specification and verification of TCP extended with the Window Scale Option Science of Computer Programming, 118. pp. 3-23.

Full text not available from this repository.


We formally verify that TCP satisfies its requirements when extended with the Window Scale Option. With the aid of our μCRL specification and the LTSmin toolset, we verify that our specification of unidirectional TCP Data Transfer extended with the Window Scale Option does not deadlock, and that its external behaviour is branching bisimilar to a FIFO queue for a significantly large instance. Separately, we verify that a connection may only be closed if both entities accept the CLOSE call from the Application Layer. Finally, we recommend a rewording of the specification regarding how a zero window is probed, ensuring deadlocks do not arise as a result of misinterpretation.

Item Type: Article
Subjects : Computing
Divisions : Surrey research (other units)
Authors :
Lockefeer, L
Fokkink, W
Date : 1 March 2016
DOI : 10.1016/j.scico.2015.08.005
Copyright Disclaimer : © 2015 Elsevier B.V. All rights reserved.
Uncontrolled Keywords : μCRL, Process algebra, Transmission control protocol, Window scale option, Sliding window protocol
Depositing User : Symplectic Elements
Date Deposited : 17 May 2017 13:58
Last Modified : 25 Jan 2020 00:35

Actions (login required)

View Item View Item


Downloads per month over past year

Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800