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
- 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
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.