Formal Description and Analysis of a Bounded Retransmission Protocol

Abstract : This paper reports about the formal specification and verification of a Bounded Retransmission Protocol (BRP) used by Philips in one of its products. We started with the descriptions of the BRP service (i.e., external behaviour) and protocol written in the mu-CRL language by Groote and van de Pol. After translating them in the LOTOS language, we performed verifications by model-checking using the CADP (CAESAR/ALDEBARAN) toolbox. The models of the LOTOS descriptions were generated using the CAESAR compiler (by putting bounds on the data domains) and checked to be branching equivalent using the ALDEBARAN tool. Alternately, we formulated in the ACTL temporal logic a set of safety and liveness properties for the BRP protocol and checked them on the corresponding model using our XTL generic model-checker.
Type de document :
RR-2965, INRIA. 1996
Liste complète des métadonnées
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 13:37:51
Dernière modification le : mercredi 11 avril 2018 - 01:52:13
Document(s) archivé(s) le : dimanche 4 avril 2010 - 22:06:31



  • HAL Id : inria-00073733, version 1



Radu Mateescu. Formal Description and Analysis of a Bounded Retransmission Protocol. RR-2965, INRIA. 1996. 〈inria-00073733〉



Consultations de la notice


Téléchargements de fichiers