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.

Abstract

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
Authors :
NameEmailORCID
Lockefeer, LUNSPECIFIEDUNSPECIFIED
Williams, DMd.m.williams@surrey.ac.ukUNSPECIFIED
Fokkink, WUNSPECIFIEDUNSPECIFIED
Date : 1 March 2016
Identification Number : 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 : 18 May 2017 12:54
URI: http://epubs.surrey.ac.uk/id/eprint/841025

Actions (login required)

View Item View Item

Downloads

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