Analysing The Pgm Protocol With Uppaal

Pragmatic General Multicast (PGM) is a reliable multicast protocol, designed to minimize both the probability of negative acknowledgement implosion and the load of the network due to the retransmission of lost packets. This protocol was presented to the Internet Engineering Task Force as an open reference specification. In this paper, we focus on the main reliability property which PGM intends to guarantee: a receiver either receives all data packets from transmissions and repairs or is able to detect unrecoverable data packet loss. We first propose a modelization of (a simplified version of) PGM via a network of timed automata. Using the UPPAAL model-checker, we then study the validity of the above reliability property, which does not always turn out to be verified, but to depend on the values of several parameters, which we underscore.