The Formal Verification of the Fairisle ATM Switching Element: an Overview
The work
| Authors | Paul Curzon |
|---|---|
| Editors | |
| Type | techreport |
| Year | 1994 |
| Citekey | curzon1994formalb |
Where it appeared
| Publisher | University of Cambridge Computer Laboratory |
|---|---|
| School | University of Cambridge Computer Laboratory |
| Pages | 46 |
Identifiers
| DOI | 10.48456/tr-328 |
|---|---|
| report_number | UCAM-CL-TR-328 |
Access
| URL | https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-328.html |
|---|---|
| Landing page | https://www.cl.cam.ac.uk/ftp/hvg/papers/fabric.ps.gz |
Related
| Distinct from | cabodi2016hardware |
|---|---|
| Distinct from | curzon1994formal |
| Distinct from | herbert1988case |
| Distinct from | lee2026formal |
| Distinct from | mateescu2020modeling |
| Distinct from | melham1990formalizing |
| Distinct from | wong1993formal |
From bibtex.
Abstract
We give an overview of the formal verification of an implementation of a self routing 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 outline 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.
A copy is held
pdf, 286.7 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-16 02:53 UTC |
| Approved by | a person 2026-10-02 10:03 UTC |
Cite it as
@techreport{curzon1994formalb,
title = {The Formal Verification of the Fairisle ATM Switching Element: an Overview},
author = {Paul Curzon},
year = {1994},
publisher = {University of Cambridge Computer Laboratory},
school = {University of Cambridge Computer Laboratory},
pages = {46},
doi = {10.48456/tr-328},
}
This record lives at https://refs.drheap.org/curzon1994formalb/ and will keep doing so.