Carolos Livadas and Nancy A. Lynch. A Formal Venture into Reliable Multicast Territory. Proceedings of the 22nd International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'02, Houston, TX, November, 2002), Doron A. Peled and Moshe Y. Vardi, Eds., Volume 2529 of Lecture Notes in Computer Science, Springer Verlag, pp. 146-161.
[postscript, pdf, bib]

Full version as Technical Report MIT/LCS/TR-868, Lab. for Computer Science, MIT, Cambridge, MA, Nov. 2002.

Abstract

In this paper, we present a formal model of the reliable multicast service that ensures eventual packet delivery with, possibly, some timeliness guarantees. This model dictates precisely what it means to be a member of the reliable multicast group and which packets are guaranteed delivery to which members of the group. Moreover, it is reasonable, implementable, and broad; that is, it captures the intended behavior of numerous reliable multicast protocols. We also present a formal model of the Scalable Reliable Multicast (SRM) protocol. We show that our model of SRM is safe, in the sense that it is a faithful implementation of our model of the reliable multicast service; that is, it may only deliver appropriate packets to each member of the reliable multicast group. We also show that, under certain constraints, the implementation is live, in the sense that it guarantees the timely delivery of the appropriate packets to the appropriate members of the reliable multicast group.