LIP6 1998/009

• Rapports de recherche «Une preuve formelle du bounded retransmission protocol dans le pi-calcul»
• B. Mammass
• 109 pages - 16/03/1998 - document en - http://www.lip6.fr/lip6/reports/1998/lip6.1998.009.ps.gz 179 Ko
• Contact 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.