The Formal Verification of the Fairisle ATM Switching Element: An Overview

We overview the formal verification of an implementation of a self routeing ATM switching element. This verification was performed using the HOL90 theorem proving system so is fully machine-checked. The switching element is in use in a real network, switching real data. Thus, this work constitutes a realistic formal verification case study. We give an informal overview of the switch and element and give a tutorial on the methods used. We overview how these techniques were applied to verify the switching element. We then discuss the time spent on the verification. This was comparable to the time spent designing and testing the element. Finally we describe the errors discovered. 1 Introduction Communication networks are rapidly becoming all pervasive. Systems are increasingly being networked in the local area with applications using non-local services. In the wide area telecommunications companies are turning to digital networks. As networks become all pervasive, the consequences of er..