Abstract
A data link protocol developed and used by Philips Electronics is modeled and verified using I/O automata theory. Correctness is computer-checked with the Coq proof development system.
The work of the first author is partially supported by ESPRIT Basic Research Action 6453: ‘Types for Proofs and Programs’. The work of the third author took place in the context of the ESPRIT Basic Research Action 7166: ‘CONCUR2’.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
K. Apt, N. Francez, and S. Katz. Appraising fairness in languages for distributed programming. Distributed Computing, 2:226–241, 1988.
H. Barendregt. Lambda calculi with types. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, pages 117–309. Oxford University Press, 1992.
M. Bezem and J. Groote. A formal verification of the alternating bit protocol in the calculus of constructions. Logic Group Preprint Series 88, Dept. of Philosophy, Utrecht University, Mar. 1993.
G. v. Bochmann and D. Probst, editors. Proceedings of the 4th International Conference on Computer Aided Verification, volume 663 of Lecture Notes in Computer Science. Springer-Verlag, 1992.
D. Bosscher, I. Polak, and F. Vaandrager. Verification of an audio control protocol. Report CS-R94XX, CWI, Amsterdam, 1994. In preparation.
CCITT Fascicle VIII.3. CCITT Recommendation X.25. Interface between DTE and DCE for Terminals Operating in the Packet Mode on Public Data Networks, 1988.
R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench: A semantics based tool for the verification of concurrent systems. ACM Trans. Prog. Lang. Syst., 1(15):36–72, 1993.
C. Courcoubetis, editor. Proceedings of the 5th International Conference on Computer Aided Verification, Elounda, Greece, June/July 1993, volume 697 of Lecture Notes in Computer Science. Springer-Verlag, 1993.
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, INRIA — Rocquencourt, May 1993.
U. Engberg, P. Grønning, and L. Lamport. Mechanical verification of concurrent systems with TLA. In Bochmann and Probst [4].
M. Gordon. HOL: a proof generating system for higher-order logic. In G. Birtwistle and P. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis. Kluwer Academic Publishers, 1988.
J. Groote and J. van de Pol. A bounded retransmission protocol for large data packets. Logic Group Preprint Series 100, Dept. of Philosophy, Utrecht University, Oct. 1993.
J. Guttag and J. Horning. Larch: Languages and Tools for Formal Specification. Springer-Verlag, 1993.
M. Hofmann. Extensional Concepts in Intensional Type Theory. PhD thesis, University of Edinburgh, 1994. Forthcoming.
B. Jonsson. Compositional Verification of Distributed Systems. PhD thesis, Department of Computer Systems, Uppsala University, 1987. DoCS 87/09.
L. Lamport. How to write a proof. Research Report 94, Digital Equipment Corporation, Systems Research Center, Feb. 1993.
P. Loewenstein and D. Dill. Verification of a multiprocessor cache protocol using simulation relations and higher-order logic (summary). In E. Clarke and R. Kurshan, editors, Proceedings of the 2nd International Conference on Computer-Aided Verification, New Brunswick, NJ, USA June 1990, volume 531 of Lecture Notes in Computer Science, pages 302–311. Springer-Verlag, 1991.
Z. Luo, R. Pollack, and P. Taylor. How to use LEGO. Technical Report LFCS-TN-27, University of Edinburgh, Edinburgh, Scotland, Oct. 1989.
N. Lynch and M. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the 6th Annual ACM Symposium on Principles of Distributed Computing, pages 137–151, Aug. 1987. A full version is available as MIT Technical Report MIT/LCS/TR-387.
N. Lynch and M. Tuttle. An introduction to input/output automata. CWI Quarterly, 2(3):219–246, Sept. 1989.
N. Lynch and F. Vaandrager. Forward and backward simulations — part I: Untimed systems. Report CS-R9313, CWI, Amsterdam, Mar. 1993.
S. Mauw and G. Veltink, editors. Algebraic Specification of Communication Protocols. Cambridge Tracts in Theoretical Computer Science 36. Cambridge University Press, 1993.
T. Nipkow. Formal verification of data type refinement — theory and practice. In J. de Bakker, W. d. Roever, and G. Rozenberg, editors, Proceedings REX Workshop on Stepwise Refinement of Distributed Systems: Models, Formalism, Correctness, Mook, The Netherlands, May/June 1989, volume 430 of Lecture Notes in Computer Science, pages 561–591. Springer-Verlag, 1990.
C. Paulin-Mohring. Inductive definitions in the system Coq. Rules and properties. In M. Bezem and J. Groote, editors, Proceedings of the 1st International Conference on Typed Lambda Calculi and Applications, TCLA'93, Utrecht, The Netherlands, volume 664 of Lecture Notes in Computer Science, pages 328–345. Springer-Verlag, 1993.
L. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science. Academic Press, 1989.
J. Søgaard-Andersen, S. Garland, J. Guttag, N. Lynch, and A. Pogosyants. Computer-assisted simulation proofs. In Courcoubetis [8], pages 305–319.
A. Tanenbaum. Computer networks. Prentice-Hall International, Englewood Cliffs, 1981.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Helmink, L., Sellink, M.P.A., Vaandrager, F.W. (1994). Proof-checking a data link protocol. In: Barendregt, H., Nipkow, T. (eds) Types for Proofs and Programs. TYPES 1993. Lecture Notes in Computer Science, vol 806. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58085-9_75
Download citation
DOI: https://doi.org/10.1007/3-540-58085-9_75
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58085-0
Online ISBN: 978-3-540-48440-0
eBook Packages: Springer Book Archive