Pragmatic General Multicast (PGM) Protocol.

Organisation:	University of Paris 7 and ENSEEIHT Toulouse (FRANCE)
Method:	IF
Tools used:	CADP (Construction and Analysis of Distributed Processes) IF toolbox
Domain:	Communication Protocols.
Period:	2003
Size:	up to 702,196 states and 938,857 transitions
Description:	The Pragmatic General Multicast (PGM) protocol was designed by CISCO Systems and TIBCO to support reliable multicast of small, real-time generated information (e.g., in video applications) to potentially millions of users. A session of PGM (i.e., a given data transfer from a source to a group of receivers) builds a tree having the source as root, the receivers as leaves, and other network elements as intermediate nodes. The tree may change during the session due to the dynamic join/leave of receivers. In the normal course of a data transfer, the source multicasts sequenced data packets (ODATA) along a path of the tree to the receivers. When a receiver detects missing data packets from the expected sequence, it unicasts repeatedly to the last network element of the path negative achnowledgements (NAKs) containing the sequence number of missing data. Network elements forward NAKs hop-by-hop to the source using the reverse path, and confirm each hop by multicasting a NAK confirmation (NCF) in response to the child from which the NAK was received. Receivers and network elements stop sending NAKs at the reception of a corresponding NCF. Finally, the source itself receives and confirms the NAK by multicasting an NCF to the group. If the data missing is still in memeory, repairs (RDATA) may be provided by the source in response to the NAK. To avoid NAK implosion (prohibitive number of NAK messages), PGM specifies procedures for NAK elimination within network elements in order to propagate just one copy of a given NAK along the reverse of the distribution path. PGM does not intend to always guarantee full reliability, but rather to ensure the following property: a receiver either receives all data packets from transmissions and repairs, or it is able to detect unrecoverable data packet loss. This work studies under which conditions (i.e., settings of the protocol parameters) full reliability is obtained. The methodology proposed consists of several steps: Abstraction of the PGM parameters in order to obtain a model sufficiently simple to be handled by existing model checking tools, and sufficiently realistic to preserve the full reliability property. Several dimensions of the PGM complexity (topology, policy of loss, communication network, length of the information transmitted, shape of the traffic, mechanisms to ensure efficiency, and management of the transmission window) are examined carefully, and for each one appropriate abstractions of the relevant PGM parameters are proposed. Based on these abstractions, a parameterized PGM model was built in IF. The source, receiver, and network element are modelled as timed automata with counter variables. Analysis of the sequence of events (recovery of a loss) needed to obtain the target property (full reliability). This sequence involves four steps: loss of ODATA packets by a node; reception of a packet by the receiver signaling that previous data packets have been lost; reception of the NAK by the source while the corresponding data is still in the transmission window; and transmission of the corresponding repair RDATA. After analysing the different aspects of the PGM model involved by this sequence of events, a non-linear constraint on the PGM parameters is synthesized, which ensures the recovery of a lost data packet. Verification of the constraint obtained using finite timed model checking. This consists of several actions: assignment of relevant values to the PGM parameters; instantiation of the abstract model into a concrete model; translation of this model into a Labelled Transition System (LTS) encoded in the BCG format; verification of basic properties (deadlock freedom, absence of overflows, etc.); translation of the parameterized property ensuring the constraint into a set of concrete properties, formulated in regular alternation-free mu-calculus, obtained by instantiating sequence numbers; and verification of these properties on the LTS using the EVALUATOR model checker of CADP. The full series of experiments (approximately 300 cases) resulting from different parameter instantiations were performed in 4 hours on a PC at 1GHz and 1Gbyte of memory. The results obtained by model checking confirmed that the constraint synthesized indeed guarantees the full reliability of the PGM protocol.
Conclusions:	The verification and synthesis problems for parameterized systems are difficult when the parameters are related by non-linear constraints. The proposed methodology allows to use finite and real-time model checking do deal with such systems. The methodology was applied on a non-trivial case-study, the PGM protocol, for which an (almost complete) parameterized formal model was developed.
Publications:	[Boyer-Sighireanu-03] Marc Boyer and Mihaela Sighireanu. "Synthesis and Verification of Constraints in the PGM Protocol". In Keijiro Araki, Stefania Gnesi, and Dino Mandrioli, editors, Proceedings of the 12th International Symposium of Formal Methods Europe FME'03 (Pisa, Italy), Lecture Notes in Computer Science vol. 2805, pp. 264-281. Springer Verlag, September 2003. Available on-line at: http://www.liafa.jussieu.fr/~sighirea/PAPERS/Boyer-Sighireanu-03.ps.gz or from the CADP Web site in PDF or PostScript
Contact:	Mihaela Sighireanu Assistant Professor University of Paris 7 / LIAFA Case 7014 2, place Jussieu F-75251 Paris Cedex 05 FRANCE Tel: +(33) 1 44 27 54 19 Fax: +(33) 1 44 27 68 49 E-mail: Mihaela.Sighireanu@liafa.jussieu.fr
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page