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.
• Mots clés : protocole de communication, vue abstraite, implementation, preuve formelle, pi-calcul polyadique, bisimulation, deadlock
• Directeur de la publication : David.Massot (at) nulllip6.fr