Sciweavers

Share
ICNP
2006
IEEE

Rigorous Protocol Design in Practice: An Optical Packet-Switch MAC in HOL

9 years 11 months ago
Rigorous Protocol Design in Practice: An Optical Packet-Switch MAC in HOL
— This paper reports on an experiment in network protocol design: we use novel rigorous techniques in the design process of a new protocol, in a close collaboration between systems and theory researchers. The protocol is a Media Access Control (MAC) protocol for the SWIFT optical network, which uses optical switching and wavelength striping to provide very high bandwidth packetswitched interconnects. The use of optical switching (and the lack of optical buffering) means that the protocol must control the switch within hard timing constraints. We use higher-order logic to express the protocol design, in the general-purpose HOL automated proof assistant. The specification is thus completely precise, but still concise, readable, and without accidental overspecification. Further, we test conformance between the specification and two implementations of the protocol: an NS-2 simulation model and the VHDL code of the network hardware. This involves: (1) proving, within HOL, that the spec...
Adam Biltcliffe, Michael Dales, Sam Jansen, Tom Ri
Added 11 Jun 2010
Updated 11 Jun 2010
Type Conference
Year 2006
Where ICNP
Authors Adam Biltcliffe, Michael Dales, Sam Jansen, Tom Ridge, Peter Sewell
Comments (0)
books