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.
• Keywords : communication protocol, abstract view, implementation, formal proof, polyadic pi-calculus, bisimulation, deadlock
• Publisher : David.Massot (at) nulllip6.fr