Une preuve formelle du bounded retransmission protocol dans le pi-calcul

B. Mammass

LIP6 1998/009: Rapport de Recherche LIP6 / LIP6 research reports
109 pages - Mars/March 1998 - French document.

PostScript : 174 Ko /Kb

Contact : par mail / e-mail

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

Titre français : Une preuve formelle du bounded retransmission protocol dans le pi-calcul
Titre anglais : A formal proof of the bounded retransmission protocol in the pi-calculus

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.

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.

Mots-clés : protocole de communication, vue abstraite, implementation, 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