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
- Keywords : communication protocol, abstract view, implementation, formal proof, polyadic pi-calculus, bisimulation, deadlock
- Publisher : David.Massot (at) nulllip6.fr
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.
This work is compared to some related works on the same protocol focusing on how the used formalism influences implementation choices and proof techniques.