Formal specification and verification of TCP extended with the window scale option

L. Lockefeer, D.M. Williams, W. Fokkink

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

7 Citations (Scopus)

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 verified that our specification of unidirectional TCP 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. 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
Title of host publicationFormal Methods for Industrial Critical Systems - 19th International Conference, FMICS 2014, Proceedings
EditorsF. Lang, F. Flammini
PublisherSpringer
Pages63-77
Number of pages15
VolumeCham
ISBN (Electronic)978-3-319-10702-8
ISBN (Print)978-3-319-10701-1
DOIs
Publication statusPublished - 2014
Externally publishedYes
Event19th International Conference on Formal Methods for Industrial Critical Systems (FMICS 2014) - Florence, Italy
Duration: 11 Sep 201412 Sep 2014
Conference number: 19

Publication series

NameLecture Notes in Computer Science
Volume8718
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference19th International Conference on Formal Methods for Industrial Critical Systems (FMICS 2014)
Abbreviated titleFMICS 2014
CountryItaly
CityFlorence
Period11/09/1412/09/14

Fingerprint Dive into the research topics of 'Formal specification and verification of TCP extended with the window scale option'. Together they form a unique fingerprint.

Cite this