Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 5 Aug 1994 17:27:19 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA17511; Fri, 5 Aug 1994 10:10:52 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA17449; Fri, 5 Aug 1994 10:10:34 -0600 Received: from coot.cl.cam.ac.uk (user pc (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Fri, 5 Aug 1994 17:06:33 +0100 To: info-hol@leopard.cs.byu.edu Subject: Switching element verification technical reports Date: Fri, 05 Aug 94 17:06:25 +0100 From: Paul Curzon Message-Id: <"swan.cl.cam.:049900:940805160645"@cl.cam.ac.uk> The following technical reports are now available by anonymous ftp from the Cambridge ftp site: ftp.cl.cam.ac.uk in directory hvg/papers FILE: fabric.ps.gz The Formal Verification of the Fairisle ATM Switching Element: an Overview Paul Curzon Technical Report 328, University of Cambridge, Computer Laboratory, 1994. 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. The literate specifications can be found in a separate report (below). FILE: LitFabric.ps.gz The Formal Verification of the Fairisle ATM Switching Element Paul Curzon Technical Report 329, University of Cambridge Computer Laboratory, 1994. This report contains the literate specifications of the verification described in the above report. We give all the definitions used in the verification with accompanying documentation together with the main correctness theorems proved. These reports can also be accessed from my WWW home page which contains other information about the Fairisle verification project. URL: http://www.cl.cam.ac.uk/users/pc/ Paul Curzon University of Cambridge Computer Laboratory pc@cl.cam.ac.uk