Issue No.04 - April (1991 vol.40)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/12.88464
<p>A communication protocol is stabilizing if and only if starting from any unsafe state (i.e. one that violates the intended invariant of the protocol), the protocol is guaranteed to converge to a safe state within a finite number of state transitions. Stabilization allows the processes in a protocol to reestablish coordination between one another whenever coordination is lost due to some failure. The authors identify some important characteristics of stabilizing protocols; they show in particular that a stabilizing protocol is nonterminating, has an infinite number of safe states, and has timeout actions. They also propose a formal method for proving protocol stabilization: in order to prove that a given protocol is stabilizing, it is sufficient (and necessary) to exhibit and verify what is called a 'convergence stair' for the protocol. Finally, they discuss how to redesign a number of well-known protocols to make them stabilizing; these include the sliding-window protocol and the two-way handshake.</p>
communication protocol stabilization; state transitions; safe states; formal method; convergence stair; sliding-window protocol; two-way handshake; formal specification; program verification; protocols.
M.G. Gouda, N.J. Multari, "Stabilizing Communication Protocols", IEEE Transactions on Computers, vol.40, no. 4, pp. 448-458, April 1991, doi:10.1109/12.88464