Experiences formally verifying a network component

Author

Curzon, Paul

Author_Institution

Comput. Lab., Cambridge Univ., UK

fYear

1994

fDate

27 Jun-1 Jul 1994

Firstpage

183

Lastpage

193

Abstract

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

Keywords

asynchronous transfer mode; formal specification; formal verification; switching networks; theorem proving; Asynchronous Transfer Mode; Cambridge Fairisle Network; HOL90 theorem proving system; formal verification; network component; network switching fabric; Application software; Asynchronous transfer mode; Computer crashes; Computer networks; Fabrics; Formal verification; Laboratories; Logic; Switches; Testing;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer Assurance, 1994. COMPASS '94 Safety, Reliability, Fault Tolerance, Concurrency and Real Time, Security. Proceedings of the Ninth Annual Conference on

Conference_Location

Gaithersburg, MD

Print_ISBN

0-7803-1855-2

Type

conf

DOI

10.1109/CMPASS.1994.318453

Filename

318453