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
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.