LIP6 1998/010
- Rapports de recherche
Encore et encore le bounded retransmission protocol - Th. Hardin, B. Mammass
- 18 pages - 16/03/1998- document en - http://www.lip6.fr/lip6/reports/1998/lip6.1998.010.ps.gz - 58 Ko
- Contact : Therese.Hardin (at) nulllip6.fr, Brahim.Mammass (at) nulllip6.fr
- Ancien Thème : SPI
- Mots clés : protocole de communication, vue abstraite, implémentation, preuve formelle, pi-calcul polyadique, bisimulation, deadlock
- Directeur de la publication : David.Massot (at) nulllip6.fr
Le papier présente une preuve formelle du bounded retransmission protocol. Le service offert par le protocole et le protocole lui-même sont spécifiés dans le pi-calcul polyadique. Ensuite, ces deux spécifications sont prouvées équivalentes en utilisant les techniques de bismulation du pi-calcul. Cette équivalence permet de déduire certaines propriétés du protocole telles que l'absence de deadlock.
Ce travail est comparé à d'autres travaux sur le même protocole en mettant en évidence l'influence du formalisme utilisé sur les choix d'implémentation et sur les techniques de preuve.
Ce travail est comparé à d'autres travaux sur le même protocole en mettant en évidence l'influence du formalisme utilisé sur les choix d'implémentation et sur les techniques de preuve.