Verification of XTP context management closing procedure in style of TLA

Modular specification and compositional verification of the context management closing procedure of Xpress Transfer Protocol (XTP Protocol Definition, Revision 3.6) in style of Lamportʹs Temporal Logic of Actions is considered. 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 transmitted successfully to the hosts. Thus, the case of the closing procedure is considered where both contexts are active and synchronized initially, and only control messages have to be sent until the association is closed.