Reliable Large Scale Multipoint Transport Protocol

Organisation:	TESA laboratory Toulouse (FRANCE)
Method:	TURTLE UML profile
Tools used:	CADP (Construction and Analysis of Distributed Processes) TTool
Domain:	Communication Protocols.
Period:	2004
Size:	n/a
Description:	Protocols for large scale reliable multipoint communication services have to guarantee the transmission of a message to numerous receivers. Geostationary satellites are well adapted for multipoint transmissions. However, due to the high variability of the quality of reception, ensuring reliable transmission using satellites requires the design of adapted protocols and might be more costly than classical solutions based on terrestrial transmissions. This thesis proposes a new protocol based on a hybrid approach combining the advantages of terrestrial and satellite transmissions, by choosing the more profitable network depending on a cost function. The validation the proposed solution proceeds in three steps. First the protocol is modeled using the real-time UML profile TURTLE. In a second step, the reachability graph is generated using TTool. Finally, CADP is used for model checking properties of the protocol on the reachability graph. Notice that the open interface of CADP allowed to integrate the generation and analysis of the reachability graph smoothly into TTool. The protocol has been validated using an incremental approach, adding and validating the services one-by-one. Several properties have been verified, in particular that there are neither deadlocks nor lost messages, and that the terrestrial peer-to-peer networks are used correctly. Furthermore, the behavior of the protocol was shown to be observationally equivalent to the specified service. For this last step, the features provided by CADP for transformation of the reachability graph, such as hiding unobservable communications and minimisation, proved to be crucial.
Conclusions:	A new protocol for reliable large scale multipoint transport using terrestrial and satellite transmissions is proposed. For its formal verification, the graph manipulation features offered by CADP were essential.
Publications:	[Belleville-04] Florestan de Belleville. "Transport multipoint fiable á très grande échelle : Intégration de critères de coût en environnement Internet hybride satellite / terrestre". PhD Thesis (in French). Available on-line at: http://tel.ccsd.cnrs.fr/documents/archives0/00/00/86/39/tel-00008639-01/tel-00008639.pdf or from the CADP Web site in PDF or PostScript
Contact:	Florestan de Belleville ENSEEIHT équipe IRT 2, rue Charles Camichel BP 7122 F-31071 Toulouse Cedex 7 France Tel.: +33 (0)5 61 58 50 22 E-mail: fdebelle@tesa.prd.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