Abstract
Designs are often modified for use in new circumstances. If formal proof is to be an acceptable verification methodology for industry, it must be capable of tracking design changes quickly. We describe our experiences formally verifying an implementation of an ATM network component, and on our subsequent verification of modified designs. Three of the designs verified are in use in a working network. They were designed and implemented with no consideration for formal methods. This case study gives an indication of the difficulties in formally verifying a real design and of subsequently tracking design changes.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Richard Boulton. Lazy techniques for fully-expansive theorem proving. Formal Methods in System Design, 3(1/2), August 1993.
Albert J. Camilleri. Formal methods in industry. Tutorial at the 1991 International Workshop on the HOL Theorem Proving System and its Applications.
Paul Curzon. Experiences formally verifying a network component. In Proceedings of the 9th Annual IEEE Conference on Computer Assurance. IEEE Press, 1994.
Paul Curzon. The formal verification of the Fairisle ATM switching element. Technical Report 329, University of Cambridge Computer Laboratory, 1994.
Paul Curzon. The formal verification of the Fairisle ATM switching element: an overview. Technical Report 328, University of Cambridge Computer Laboratory, 1994.
K. Edgcombe. The Qudos quick chip user guide. Qudos Limited.
Daniel Gordon. The 4 by 4 and 16 by 16 switch fabrics: Design and implementation. In ATM Document Collection 2. University of Cambridge, Computer Laboratory, February 1993.
M.J.C. Gordon and T.F. Melham. Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, 1993.
Jeffrey Joyce and Carl Seger. The HOL-Voss system: Model-checking inside a general-purpose theorem prover. In Jeffrey J. Joyce and Carl-Johan H. Seger, editors, Higher Order Logic Theorem Proving and Its Applications, 6th International Workshop, HUG'93, number 780 in Lecture Notes in Computer Science. Springer-Verlag, 1994.
I.M. Leslie and D.R. McAuley. Fairisle: An ATM network for the local area. ACM Communication Review, 19(4), September 1991.
K. L. McMillan. Symbolic Model Checking. Kluwer, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Curzon, P. (1994). Tracking design changes with formal verification. In: Melham, T.F., Camilleri, J. (eds) Higher Order Logic Theorem Proving and Its Applications. HUG 1994. Lecture Notes in Computer Science, vol 859. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58450-1_42
Download citation
DOI: https://doi.org/10.1007/3-540-58450-1_42
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58450-6
Online ISBN: 978-3-540-48803-3
eBook Packages: Springer Book Archive