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 language | English |
|---|---|
| Title of host publication | Formal Methods for Industrial Critical Systems - 19th International Conference, FMICS 2014, Proceedings |
| Editors | F. Lang, F. Flammini |
| Publisher | Springer |
| Pages | 63-77 |
| Number of pages | 15 |
| Volume | Cham |
| ISBN (Electronic) | 978-3-319-10702-8 |
| ISBN (Print) | 978-3-319-10701-1 |
| DOIs | |
| Publication status | Published - 2014 |
| Externally published | Yes |
| Event | 19th International Conference on Formal Methods for Industrial Critical Systems (FMICS 2014) - Florence, Italy Duration: 11 Sept 2014 → 12 Sept 2014 Conference number: 19 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Volume | 8718 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Conference
| Conference | 19th International Conference on Formal Methods for Industrial Critical Systems (FMICS 2014) |
|---|---|
| Abbreviated title | FMICS 2014 |
| Country/Territory | Italy |
| City | Florence |
| Period | 11/09/14 → 12/09/14 |