Formal Specification and Verification of TCP Extended with the Window Scale Option
作者： Lars Lockefeer , David M. Williams , Wan J. Fokkink
DOI: 10.1007/978-3-319-10702-8_5
关键词: Formal specification 、 Deadlock 、 Distributed computing 、 Computer science 、 Real-time computing 、 Branching (version control)
摘要: We formally verify that TCP satisfies its requirements when extended with the Window Scale Option. With aid of our μCRL specification and ltsmin toolset, we verified unidirectional Option does not deadlock, external behaviour is branching bisimilar to a FIFO queue for significantly large instance. Finally, recommend rewording regarding how zero window probed, ensuring deadlocks do arise as result misinterpretation.
springer.com
core.ac.uk
narcis.nl参考文章(21)
M. A. S. Smith, Formal verification of communication protocols formal techniques for (networked and) distributed systems. pp. 129- 144 ,(1996) , 10.1007/978-0-387-35079-0_8
Eric Madelaine, Didier Vergamini, Specification and Verification of a Sliding Window Protocol in LOTOS formal techniques for (networked and) distributed systems. pp. 495- 510 ,(1991) , 10.1016/B978-0-444-89402-1.50045-X
Tom Ridge, Michael Norrish, Peter Sewell, A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service Lecture Notes in Computer Science. pp. 294- 309 ,(2008) , 10.1007/978-3-540-68237-0_21
Nancy A. Lynch, Mark Anthony Shawn Smith, Formal verification of tcp and t/tcp Massachusetts Institute of Technology. ,(1997)
J. Postel, Transmission Control Protocol Internet Request for Comment (RFC793). ,vol. 793, pp. 1- 91 ,(1981)
Bing Han, Jonathan Billington, Termination Properties of TCP’s Connection Management Procedures Applications and Theory of Petri Nets 2005. pp. 228- 249 ,(2005) , 10.1007/11494744_14
Dmitri Chkliaev, Jozef Hooman, Erik de Vink, Verification and improvement of the sliding window protocol tools and algorithms for construction and analysis of systems. pp. 113- 127 ,(2003) , 10.1007/3-540-36577-X_9
R. Braden, Requirements for Internet Hosts - Communication Layers RFC. ,vol. 1122, pp. 1- 116 ,(1989)
V. Jacobson, D. Borman, R. Braden, TCP Extensions for High Performance TCP Extensions for High Performance. ,vol. 1323, pp. 1- 37 ,(1992)
Jonathan Billington, Bing Han, Validating TCP connection management formal methods. pp. 47- 55 ,(2002)