The formal verification of an ATM network
Paul Curzon · 1994
Communication networks are rapidly becoming all pervasive. As this occurs, the consequences of errors in the design or implementation of network components becomes increasingly important. This is especially so if, as is increasingly probable, networks are used in safety-critical applications where communication problems could cause loss of life. Asynchronous Transfer Mode (ATM) is a relatively new technology that is being adopted by both the computer and telecommunication industries. It is likely to be the most important transfer mode of the foreseeable future. It is being touted as a technology that can be used \\everywhere": in wide-area, metropolitan area, local area and even desk area networks [4]. ATM systems could become high-volume products for which high dependability is paramount. It is an important application for formal verification research. The ATM Verification Project at Cambridge is investigating the use of formal methods, and in particular the HOL system [2], to validate an implementation of an ATM Network. The network under consideration is Fairisle [3]. It is a working network, carrying real user data. It was designed and implemented with no thought for formal verification. It provides a realistic case study for the investigation of the formal verification of an ATM network. Initially, we are verifying the switch hardware using conventional machine-checked formal