Connection management for the transport layer: service specification and protocol verification

A symmetric connection management service between two service access points is specified, using a state transition system and safety and progress requirements. At each access point. the user can request connection establishment, request connection termination, and signal whether or not they are willing to accept connection requests from the remote user. The protocol can indicate connection establishment, connection termination, and rejection of a connection establishment request. The authors then specify a protocol and verify that it offers the service, given communication channels between the access points that can lose, reorder, and duplicate messages, but which guarantee delivery of a message that is repeatedly sent. The protocol achieves the service using 2-way and 3-way handshakes, and can be directly combined with any existing single-connection data transfer protocols to provide a transport layer protocol that offers both connection management and data transfer services. The protocol and service are compared to TCP and its intended service, and to ISO TP Class 4 and its intended service