Formal verification of communication protocols
作者： M. A. S. Smith
DOI: 10.1007/978-0-387-35079-0_8
关键词:
摘要: In this paper we present a formal abstract specification for TCP/IP transport level protocols and formally verify that TCP satisfies specification. We also description of an experimental protocol, T/TCP, which proposes to provide the same service as TCP, but with optimizations make it efficient transactions. further show protocol does not propose weaker protocol. Our specifications are presented using untimed automaton model, timed model. The verification is done invariant assertion simulation techniques.
springer.com
core.ac.uk
sci-hub.st 参考文章(7)
N.A. Lynch, M.R. Tuttle, An introduction to input/output automata CWI quarterly. ,vol. 2, pp. 219- 246 ,(1989)
J. S gaard-Andersen, B. Lampson, N. Lynch, Correctness of Communications Protocols, A case Study Massachusetts Institute of Technology. ,(1993)
Butler W. Lampson, Jørgen F. Søgaard-Andersen, Nancy A. Lynch, Correctness of At-Most-Once Message Delivery Protocols formal techniques for (networked and) distributed systems. pp. 385- 400 ,(1993)
Martín Abadi, Leslie Lamport, The existence of refinement mappings Theoretical Computer Science. ,vol. 82, pp. 253- 284 ,(1991) , 10.1016/0304-3975(91)90224-P
S.L. Murphy, A.U. Shankar, Connection management for the transport layer: service specification and protocol verification IEEE Transactions on Communications. ,vol. 39, pp. 1762- 1775 ,(1991) , 10.1109/26.120163
D. Belsnes, Single-Message Communication IEEE Transactions on Communications. ,vol. 24, pp. 190- 194 ,(1976) , 10.1109/TCOM.1976.1093283
N. Lynch, F. Vaandrager, Forward and backward simulations I.: untimed systems Information & Computation. ,vol. 121, pp. 214- 233 ,(1995) , 10.1006/INCO.1995.1134