Date: Mon, 28 Mar 2005 20:38:29 +0100 From: Peter Sewell <Peter.Sewell@cl.cam.ac.uk> To: freebsd-net@freebsd.org Subject: Rigorous specification for TCP, UDP, and Sockets Message-ID: <E1DG04E-0001F2-00@mta1.cl.cam.ac.uk>
next in thread | raw e-mail | index | archive | help
[apologies to anyone who has seen this on the end-to-end list] Our recent technical reports may be of interest to BSD TCP/IP developers: TCP, UDP, and Sockets: rigorous and experimentally-validated behavioural specification. Volume 1: Overview UCAM-CL-TR-624 Volume 2: The Specification UCAM-CL-TR-625 They are available from <http://www.cl.cam.ac.uk/users/pes20/Netsem/index.html> together with the summary paper: Rigorous specification and conformance testing techniques for network protocols, as applied to TCP, UDP, and Sockets. These give a detailed and precise specification of the behaviour of three common TCP/IP stacks - versions of FreeBSD, Linux, and Windows XP - as seen from socket calls and the wire interface. The specification has been validated through extensive testing (primarily against FreeBSD for the TCP aspects). It models the actual observed behaviour, bugs and all, rather than an idealisation of the RFCs. The specification is annotated for the non-specialist reader, and we hope that it will be useful as an informal reference for stack implementors and for sockets users (supplementing the existing RFCs and books), as well as supporting automated conformance testing. Our techniques may be useful in the development of new protocols and extensions. We would greatly appreciate feedback, on both content and usability. Peter, for the Netsem team: Steve Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael Smith, Keith Wansbrough
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?E1DG04E-0001F2-00>