Yet Yet on the bounded retransmission protocol

Encore et encore le bounded retransmission protocol

Thérèse Hardin (1) , Brahim Mammass (1)

1 SPI - Sémantiques, preuves et implantation

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.

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. Ce travail est comparé à d'autres travaux sur le même protocole en mettant en évidence l'influence du formalisme utilisé sur les choix d'implémentation et sur les techniques de preuve.

Mots clés: communication protocol; abstract view; implementation; formal proof; polyadic pi-calculus; bisimulation; deadlock

Mots clés: protocole de communication; vue abstraite; implémentation; preuve formelle; pi-calcul polyadique; bisimulation; deadlock

Domaines: Informatique [cs]

Thérèse Hardin, Brahim Mammass. Yet Yet on the bounded retransmission protocol. [Research Report] lip6.1998.010, LIP6. 1998. ⟨hal-02547714⟩