A verified connection management protocol for the transport layer

摘要: We specify and verify a connection management protocol for use between entities connected by channels that can lose, reorder, duplicate messages. The is symmetric. Each entity in one of the following states: closed, listen, open, active opening, passive or closing. first three are stable states to be exited only user request, while last transient states. maintains local incarnation number at all times, remote when Our employs 3-way handshake used TCP ISO Transport Protocol (Class 4).We safety property an its matches entity's number. This ensures data messages from past instances not delivered user. progress properties: actively opening will eventually establish connection, provided willing communicate itself opening; closing transient; if remain become empty, assuming have maximum lifetime.This specification immediately combined with transfer specifications presented [SHAN1, SHAN2, SHAN3] provide transport layer functions two-way transfer. verifications too hierarchical verification multi-function protocol. because protocols images illustrates power projections constructing protocols.