Formal validation of a multicast transport protocol

The past years have seen the emergence of cooperative applications that require the exchange of high volumes of data among remote cooperating parties. With the purpose of providing a scalable communication solution for this kind of applications, multicast transport protocols have been proposed in the literature, because point to point communications lead to wasting too much bandwidth, in particular if one wants to guarantee a certain level of reliability. In this paper, we study a multicast transport protocol, scalable probabilistic reliable multicast (SPRM), and show how a formal description technique, RT-LOTOS, has been successfully applied to identify some flaws in this complex multi-parties protocol. It is shown how the same approach may also be used for performance evaluation, and we compare our results with other models based on queuing theory