Online Version - Last Updated - 20 Jan 2012 |
 |
| Home |
| |
| Procedures and Resources for Authors |
|
| Information and Resources for Volume Editors |
| |
| Orders and Subscriptions |
| |
| Published Articles |
|
| Upcoming Volumes |
| |
| Contact Us |
| |
| Useful External Links |
| |
| CRPIT Site Search |
Validating TCP Connection Management
Han, B. and Billington, J.
The Internet's Transmission Control Protocol (TCP) is specified informally in Request For Comments (RFC) 793 but still lacks a formal specification. This paper presents a formal model of TCP connection management using coloured Petri news (CPNs). The model is used to examine certain properties (e.g., the absence of deadlocks and correct message sequences) of TCP and to check the internal consistency of RFC 793. In this paper, problems with some informal descriptions in RFC 793 concerning simultaneous open have been discovered through automated reachability analysis. Corrections to the problems have been proposed and tested.
Cite as: Han, B. and Billington, J. (2002). Validating TCP Connection Management. In Proc. Workshop on Software Engineering and Formal Methods 2002, Adelaide, Australia. CRPIT, 12. Lakos, C., Esser, R., Kristensen, L. M. and Billington, J., Eds. ACS. 47-55.
(from crpit.com)
(local if available)
