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

Lars Lockefeer, David M. Williams, Wan Fokkink

Research output: Contribution to JournalArticleAcademicpeer-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 languageEnglish
Pages (from-to)3-23
Number of pages21
JournalScience of Computer Programming
Volume118
DOIs
Publication statusPublished - 1 Mar 2016

Fingerprint

Specifications
Data transfer
Formal specification
Formal verification

Keywords

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

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 = "3",
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",

}

Formal specification and verification of TCP extended with the Window Scale Option. / Lockefeer, Lars; Williams, David M.; Fokkink, Wan.

In: Science of Computer Programming, Vol. 118, 01.03.2016, p. 3-23.

Research output: Contribution to JournalArticleAcademicpeer-review

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 - http://www.scopus.com/inward/record.url?scp=84939863365&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84939863365&partnerID=8YFLogxK

U2 - 10.1016/j.scico.2015.08.005

DO - 10.1016/j.scico.2015.08.005

M3 - Article

VL - 118

SP - 3

EP - 23

JO - Science of Computer Programming

JF - Science of Computer Programming

SN - 0167-6423

ER -