Abstract
In this paper we present a formal abstract specification for TCP/IP transport level protocols and formally verify that TCP satisfies this specification. We also present a formal description of an experimental protocol, T/TCP, which proposes to provide the same service as TCP, but with optimizations to make it efficient for transactions. We further show that this protocol does not provide the same service as TCP, and propose a weaker specification for this protocol. Our specifications are presented using an untimed automaton model, and we present the protocols using a timed automaton model. The formal verification is done using invariant assertion and simulation techniques.
Supported by Air Force Contract AFOSR F49620-92-J-0125, NSF contract 9225124CCR,and ARPA contracts N00014-92-J-4033,F19628-95-C-0118,and DABT63-94-C-007
Chapter PDF
Similar content being viewed by others
References
Abadi, M. and Lamport, L. (1991) The existence of refinement mappings. Theoretical Computer Science, 82 (2): 253–284.
Belsnes, D. (1976) Single message communication. IEEE Transactions on Communications, 24 (2).
Braden, R. (1992) Extending TCP for transactions — concepts. Internet RFC-1379.
Braden, R. (1994) T/TCP — TCP extensions for transactions — functional specification. Internet RFC-1644.
Braden, R. and Clark, D. (1993) Transport protocols for transactions and streaming. Unpublished manuscript.
Lampson, B., Lynch N, and Sdgaard-Andersen, J. (1993) Correctness of at-most-once message delivery protocols. In FORTE’93–Sixth International Conference on Formal Description Techniques, pages 387–402, Boston, MA.
Lynch, N. and Tuttle, M. (1989) An introduction to input/output automata. CWI Quarterly, 3 (2).
Lynch, N. and Vaandrager, F. (1995) Forward and backward simulations - part I I: Time-based systems. To Appear in Information and Computation.
Lynch, N. and Vaandrager, F. (1993) Forward and backward simulations - part I: Untimed systems. Technical Memo MIT/LCS/TM-486, M.I.T..
Murphy, S. (1996) Private communication.
Murphy, S. and Shankar, A. (1989) Connection management for the transport layer: Service specification and protocol verification. Technical Report UMIACS-TR-88–45.1, University of Maryland, June 1988. Revised December. 1989.
Postel, J. (1981) Transmission conrol protocol - DARPA Internet program specification (Internet standard STC-007). Internet RFC-793.
Sdgaard-Anderson, J., Lynch, N. and Lampson, B. (1993) Correctness of communications protocols, a case study. Technical Report MIT/LCS/TR-589, M.I.T..
Smith, M. (1996) Formal Verification of Communications Protocols for Data Streaming and Transactions. PhD thesis, M.I.T. In progress.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Smith, M.A.S. (1996). Formal Verification of Communication Protocols. In: Gotzhein, R., Bredereke, J. (eds) Formal Description Techniques IX. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35079-0_8
Download citation
DOI: https://doi.org/10.1007/978-0-387-35079-0_8
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2883-4
Online ISBN: 978-0-387-35079-0
eBook Packages: Springer Book Archive