LIP6 1998/010

• Reports «Encore et encore le bounded retransmission protocol»
• Th. Hardin, B. Mammass
• 18 pages - 03/16/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
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. This work is compared to some related works on the same protocol focusing on how the used formalism influences implementation choices and proof techniques.