Yet Yet on the bounded retransmission protocol

Th. Hardin, B. Mammass

LIP6 1998/010: Rapport de Recherche LIP6 / LIP6 research reports
18 pages - Mars/March 1998 - Document en anglais.

PostScript : 57 Ko /Kb

Contact : par mail / e-mail

Thème/Team: Sémantique, Preuve et Implantation

Titre français : Encore et encore le bounded retransmission protocol
Titre anglais : Yet Yet on the bounded retransmission protocol

Résumé : 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.

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

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

Key-words : communication protocol, abstract view, implementation, formal proof, polyadic pi-calculus, bisimulation, deadlock

Publications internes LIP6 1998 / LIP6 research reports 1998

Responsable Éditorial / Editor
webmaster@lip6.fr