Abstract
We have embedded the meta-theory of I/O automata, a model for describing and reasoning about distributed systems, in Isabelle's version of higher order logic. On top of that, we have specified and verified a recent network transmission protocol which achieves reliable communication using single-bit-header packets over a medium which may reorder packets arbitrarily.
Research supported by ESPRIT BRA 6453, TYPES
Research supported by DFG grant Br 887/4-2, Deduktive Programmentwicklung
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Martin Abadi and Leslie Lamport. The existence of refinement mappings. In Proc. 3rd IEEE Symp. Logic in Computer Science, pages 165–177. IEEE Computer Society Press, 1988.
Yehuda Afek, Hagit Attiya, Alan Fekete, Michael Fischer, Nancy Lynch, Yishay Mansour, Da-Wei Wang, and Lenore Zuck. Reliable communication over unreliable channels. Journal of the ACM. To appeal.
Hagit Attiya, Alan Fekete, Michael Fischer, Nancy Lynch, Yishay Mansour, Da-Wei Wang, and Lenore Zuck. Reliable communication over unreliable channels. Draft version, 1990.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J.Hwang. Symbolic model checking: 1020 states and beyond. In Proc. 5th IEEE Symp. Logic in Computer Science, pages 428–439, 1990.
G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The Coq proof assistant user's guide version 5.8. Technical Report 154, INRIA, May 1993.
Leen Helmink, Alex Sellink, and Frits Vaandrager. Proof-checking a data link protocol. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs, volume 806 of Lect. Notes in Comp. Sci., pages 127–165. Springer-Verlag, 1994.
Victor Luchangco, Ekrem Söylemez, Stephen Garland, and Nancy Lynch. Verifying timing properties of concurrent algorithms. In FORTE'94: Seventh International Conference on Formal Description Techniques for Distributed Systems and Communciations Protocols, 1994. Submitted for publication.
Nancy Lynch, Michael Merritt, William Weihl, and Alan Fekete. Atomic Transactions. Morgan Kaufmann Publishers, 1994.
Nancy Lynch and Mark Tuttle. An introduction to Input/Output automata. CWI Quarterly, 2(3):219–246, 1989.
Tobias Nipkow. Formal verification of data type refinement — theory and practice. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, volume 430 of Lect. Notes in Comp. Sci., pages 561–591. Springer-Verlag, 1990.
Lawrence C. Paulson. A fixedpoint approach to implementing (co)inductive definitions. In Alan Bundy, editor, Proc. 12th Int. Conf. Automated Deduction, volume 814 of Lect. Notes in Comp. Sci., pages 148–161. Springer-Verlag, 1994.
Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lect. Notes in Comp. Sci. Springer-Verlag, 1994.
Jørgen Søgaard-Andersen, Stephen Garland, John Guttag, Nancy Lynch, and Anya Pogosyants. Computer-assisted simulation proofs. In Fourth Conference on Computer-Aided Verification, volume 697 of Lect. Notes in Comp. Sci., pages 305–319. Springer-Verlag, 1993.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nipkow, T., Slind, K. (1995). I/O automata in Isabelle/HOL. In: Dybjer, P., Nordström, B., Smith, J. (eds) Types for Proofs and Programs. TYPES 1994. Lecture Notes in Computer Science, vol 996. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60579-7_6
Download citation
DOI: https://doi.org/10.1007/3-540-60579-7_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60579-9
Online ISBN: 978-3-540-47770-9
eBook Packages: Springer Book Archive