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

Lars Lockefeer; David M. Williams; Wan Fokkink

doi:10.1016/j.scico.2015.08.005

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

Lars Lockefeer
, David M. Williams
, Wan Fokkink^*

^*Corresponding author for this work

Research output: Contribution to Journal › Article › Academic › peer-review

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.

Original language	English
Pages (from-to)	3-23
Number of pages	21
Journal	Science of Computer Programming
Volume	118
DOIs	https://doi.org/10.1016/j.scico.2015.08.005
Publication status	Published - 1 Mar 2016

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

SDG 7 Affordable and Clean Energy

Keywords

Process algebra
Sliding window protocol
Transmission control protocol
Window scale option
μCRL

Access to Document

10.1016/j.scico.2015.08.005

Persistent URL (handle)

Persistent link

Cite this

@article{f7e6569b4d714901a441dc1c1ce1fe65,

title = "Formal specification and verification of TCP extended with the Window Scale Option",

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.",

keywords = "Process algebra, Sliding window protocol, Transmission control protocol, Window scale option, μCRL",

author = "Lars Lockefeer and Williams, \{David M.\} and Wan Fokkink",

year = "2016",

month = mar,

day = "1",

doi = "10.1016/j.scico.2015.08.005",

language = "English",

volume = "118",

pages = "3--23",

journal = "Science of Computer Programming",

issn = "0167-6423",

publisher = "Elsevier B.V.",

}

TY - JOUR

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

AU - Lockefeer, Lars

AU - Williams, David M.

AU - Fokkink, Wan

PY - 2016/3/1

Y1 - 2016/3/1

N2 - 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.

AB - 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.

KW - Process algebra

KW - Sliding window protocol

KW - Transmission control protocol

KW - Window scale option

KW - μCRL

UR - https://www.scopus.com/pages/publications/84939863365

UR - https://www.scopus.com/pages/publications/84939863365#tab=citedBy

U2 - 10.1016/j.scico.2015.08.005

DO - 10.1016/j.scico.2015.08.005

M3 - Article

AN - SCOPUS:84939863365

SN - 0167-6423

VL - 118

SP - 3

EP - 23

JO - Science of Computer Programming

JF - Science of Computer Programming

ER -

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

Abstract

UN SDGs

Keywords

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this