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...

• Type: Conference
• Year: 2006
• Where: ICNP
• Authors: Adam Biltcliffe, Michael Dales, Sam Jansen, Tom Ridge, Peter Sewell
• Keywords: ICNP 2006, Network Protocol Design, Network Protocols, Optical Switching, Protocol Design