Rigorous Protocol Design in Practice: An Optical Packet-Switch MAC in HOL. - Adam Biltcliffe; Michael Dales; Sam Jansen; Tom Ridge; Peter Sewell (ICNP, 2006)