Abstract:

We consider the specification of the context management closing procedure of Xpress Transfer Protocol (XTP) in the style of Lamport's Temporal Logic of Actions. It is assumed that a full-duplex association over a pair of lossy channels between two contexts on different hosts is being closed, such that any data for that connection have already been delivered successfully to the hosts. Thus, only the case of the closing procedure is considered where both contexts are active and synchronized initially, and only control messages are needed until the association is closed.