Rigorous protocol design in practice: an optical packet-switch MAC in HOL

We report 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 packet-switched 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 specification is equivalent to an algorithmically-checkable version; (2) using automatic code-extraction to generate a testing oracle; and (3) applying that oracle to traces of the implementation. This design-time use of rigorous methods has resulted in a protocol that is better specified and more correct than it would otherwise be, with relatively little effort.