Brent Hailpern, Tien Huynh, et al.
IEEE Transactions on Software Engineering
Aho, Ullman, and Yannakakis have proposed a set of protocols that ensure reliable transmission of data across an error-prone channel. They have obtained lower bounds on the complexity required of the protocols to assure reliability for different classes of errors. They specify these protocols with finite-state machines. Although the protocol machines have only a small number of states, they are nontrivial to prove correct. This paper present proofs of one of these protocols using the finite-state-machine approach and the abstract-program approach. It also shows that the abstract-program approach gives special insight into the operation of the protocol.
Brent Hailpern, Tien Huynh, et al.
IEEE Transactions on Software Engineering
Nissim Francez, Brent Hailpern
PODC 1982
Brent Hailpern, Andrew Heller, et al.
IEEE J-SAC
W.A. Kellogg, J.T. Richards, et al.
IBM Systems Journal