-
Engineering with Logic: Rigorous Test-Oracle Specification and
Validation for TCP/IP and the Sockets API.
Steve Bishop, Matthew Fairbairn, Hannes Mehnert, Michael Norrish, Tom
Ridge, Peter Sewell, Michael Smith, and Keith Wansbrough.
J. ACM, 66(1):1:1--1:77, December 2018.
[ bib |
doi |
project page |
pdf |
http |
abstract ]
-
TCP, UDP, and Sockets: Volume 3: The Service-level
Specification.
Thomas Ridge, Michael Norrish, and Peter Sewell.
Technical Report UCAM-CL-TR-742, University of Cambridge, Computer
Laboratory, February 2009.
305pp.
[ bib |
project page |
pdf ]
-
A rigorous approach to networking: TCP, from implementation
to protocol to service.
Tom Ridge, Michael Norrish, and Peter Sewell.
In FM 2008.
[ bib |
doi |
project page |
ps |
pdf |
http |
abstract ]
-
Rigorous Protocol Design in Practice: An Optical Packet-Switch
MAC in HOL.
Adam Biltcliffe, Michael Dales, Sam Jansen, Thomas Ridge, and Peter
Sewell.
In ICNP 2006, See also the SWIFT MAC Protocol: HOL Specification at
http://www.cl.cam.ac.uk/~pes20/optical/spec.pdf.
[ bib |
doi |
project page |
ps |
pdf |
http |
abstract ]
-
Engineering with Logic: HOL Specification and
Symbolic-Evaluation Testing for TCP Implementations.
Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell,
Michael Smith, and Keith Wansbrough.
In POPL 2006.
[ bib |
doi |
project page |
ps |
pdf |
http ]
-
Rigorous specification and conformance testing techniques for
network protocols, as applied to TCP, UDP, and Sockets.
Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell,
Michael Smith, and Keith Wansbrough.
In SIGCOMM 2005.
[ bib |
doi |
project page |
ps |
pdf |
http |
abstract ]
-
An approximation to the real TCP state diagram,
Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, Michael
Smith, and Keith Wansbrough, March 2005.
This is a poster with a version of the "TCP state diagram" extracted
from the specification. It is rather more complete than the usual diagram,
but is still a very abstract and simplified view of the state space of our
specification. It is intended to be printed at A1 size or bigger.
[ bib |
project page |
ps |
pdf ]
-
TCP, UDP, and Sockets: rigorous and
experimentally-validated behavioural specification. Volume 2: The
Specification..
Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell,
Michael Smith, and Keith Wansbrough.
Technical Report UCAM-CL-TR-625, Computer Laboratory, University of
Cambridge, March 2005.
386pp.
[ bib |
project page |
ps |
pdf |
.html |
abstract ]
-
TCP, UDP, and Sockets: rigorous and
experimentally-validated behavioural specification. Volume 1:
Overview.
Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell,
Michael Smith, and Keith Wansbrough.
Technical Report UCAM-CL-TR-624, Computer Laboratory, University of
Cambridge, March 2005.
88pp.
[ bib |
project page |
ps |
pdf |
.html |
abstract ]
-
The TCP Specification: A Quick Introduction,
Steven Bishop, Matthew Fairbairn, Michael Norrish, Peter Sewell, and Keith
Wansbrough, 2004.
[ bib |
project page |
ps |
pdf ]
-
Rigour is good for you, and feasible: reflections on formal
treatments of C and UDP sockets..
Michael Norrish, Peter Sewell, and Keith Wansbrough.
In SIGOPS EW 2002.
[ bib |
doi |
project page |
ps |
pdf |
http |
abstract ]
-
Timing UDP: mechanized semantics for sockets, threads and
failures.
Keith Wansbrough, Michael Norrish, Peter Sewell, and Andrei
Serjantov.
In ESOP 2002.
[ bib |
doi |
project page |
ps |
pdf |
http |
abstract ]
-
The UDP Calculus: Rigorous Semantics for Real
Networking.
Andrei Serjantov, Peter Sewell, and Keith Wansbrough.
In TACS 2001.
[ bib |
doi |
project page |
ps |
pdf |
http |
abstract ]
-
Timing UDP: The HOL Model, Michael Norrish,
Andrei Serjantov, Peter Sewell, and Keith Wansbrough, July 2001.
http://www.cl.cam.ac.uk/users/pes20/Netsem/index.html.
[ bib |
project page |
.html ]
-
The UDP Calculus: Rigorous Semantics for Real
Networking.
Andrei Serjantov, Peter Sewell, and Keith Wansbrough.
Technical Report UCAM-CL-TR-515, Computer Laboratory, University of
Cambridge, July 2001.
iv+70pp.
[ bib |
project page |
ps |
pdf |
.html |
abstract ]