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 :
Rapport
RR-2965, INRIA. 1996
Liste complète des métadonnées

https://hal.inria.fr/inria-00073733
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

Fichiers

Identifiants

  • HAL Id : inria-00073733, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

131

Téléchargements de fichiers

187