LIP6 1998/009

• Reports «Une preuve formelle du bounded retransmission protocol dans le pi-calcul»
• B. Mammass
• 109 pages - 03/16/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
This paper presents a formal proof of the bounded retransmission protocol. The service provided by the protocol and the protocol itself are specified in the polyadic pi-calculus. Then, these two specifications are proved equivalent by using bisimulation techniques from pi-calculus. This equivalence allows to conclude some properties of the protocol like the deadlock-freeness.