Experiences formally verifying a network component

Errors in network components can have disastrous effects so it is important that all aspects of the design are correct. We describe our experiences formally verifying an implementation of an Asynchronous Transfer Mode (ATM) network switching fabric using the HOL90 theorem proving system. The design has been fabricated and is in use in the Cambridge Fairisle Network. It was designed and implemented with no consideration for formal specification or verification. This case study gives an indication of the difficulties in formally verifying real designs. We discuss the time spent on the verification. This was comparable to the time spent designing and testing the fabric. We also describe the problems encountered and the errors discovered