TESA laboratory Toulouse (FRANCE)
TURTLE UML profile
CADP (Construction and Analysis of Distributed Processes)
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.
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
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
Florestan de Belleville
ENSEEIHT équipe IRT
2, rue Charles Camichel
F-31071 Toulouse Cedex 7
Tel.: +33 (0)5 61 58 50 22
|This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies