Connection management for the transport layer: service specification and protocol verification
作者： S.L. Murphy , A.U. Shankar
DOI: 10.1109/26.120163
关键词: Best-effort delivery 、 Transport layer 、 Computer network 、 Message passing 、 Telecommunications service 、 Telecommunications network 、 OSI model 、 Computer science 、 Intelligent Network 、 Service (business) 、 Protocol (object-oriented programming)
摘要: A symmetric connection management service between two access points is specified, using a state transition system and safety progress requirements. At each point. the user can request establishment, termination, signal whether or not they are willing to accept requests from remote user. The protocol indicate rejection of establishment request. authors then specify verify that it offers service, given communication channels lose, reorder, duplicate messages, but which guarantee delivery message repeatedly sent. achieves 2-way 3-way handshakes, be directly combined with any existing single-connection data transfer protocols provide transport layer both services. compared TCP its intended ISO TP Class 4 service. >
researchgate.net 
sci-hub.se 参考文章(14)
Sandra Lynn Murphy, Service specification and protocol construction for a layered architecture University of Maryland at College Park. ,(1990)
A. Udaya Shankar, Simon S. Lam, Construction of network protocols by stepwise refinement rex workshop on stepwise refinement of distributed systems models formalisms correctness. ,vol. 430, pp. 669- 695 ,(1989) , 10.1007/3-540-52559-9_83
James F. Kurose, The Specification and Verification of a Connection Establishment Protocol Using Temporal Logic Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification. pp. 43- 62 ,(1982)
Susan Owicki, David Gries, An axiomatic proof technique for parallel programs I Acta Informatica. ,vol. 6, pp. 319- 340 ,(1976) , 10.1007/BF00268134
A. Udaya Shankar, Verified data transfer protocols with variable flow control ACM Transactions on Computer Systems. ,vol. 7, pp. 281- 316 ,(1989) , 10.1145/65000.65003
A. Udaya Shankar, Simon S. Lam, A stepwise refinement heuristic for protocol construction ACM Transactions on Programming Languages and Systems. ,vol. 14, pp. 417- 461 ,(1992) , 10.1145/129393.129394
Simon S. Lam, A. Udaya Shankar, Protocol Verification via Projections IEEE Transactions on Software Engineering. ,vol. SE-10, pp. 325- 342 ,(1984) , 10.1109/TSE.1984.5010246
Wolfgang JÜrgensen, Son T. Vuong, Formal specification and validation of ISO transport protocol components, using petri nets acm special interest group on data communication. ,vol. 14, pp. 75- 82 ,(1984) , 10.1145/639624.802063
S. L. Murphy, A. U. Shankar, A verified connection management protocol for the transport layer acm special interest group on data communication. ,vol. 17, pp. 110- 125 ,(1987) , 10.1145/55482.55495
Carl A. Sunshine, Yogen K. Datal, Connection management in transport protocols Computer Networks. ,vol. 2, pp. 454- 473 ,(1978) , 10.1016/0376-5075(78)90053-3