University of Paris 7 and ENSEEIHT Toulouse (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
up to 702,196 states and 938,857 transitions
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:
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.
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
University of Paris 7 / LIAFA
2, place Jussieu
F-75251 Paris Cedex 05
Tel: +(33) 1 44 27 54 19
Fax: +(33) 1 44 27 68 49
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|