Database of Case Studies Achieved Using CADP

Philips' Bounded Retransmission Protocol

Organisation: INRIA Rhone-Alpes

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Communication protocols.

Period: April 1996, (Approximately one week)

Size: 350 lines of source LOTOS code

Description: We performed 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 muCRL language by Groote and van de Pol. After translating them in LOTOS, 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.

Conclusions: We successfully applied the model-checking approach to this case-study. Thus, we were able to verify the correctness of the specification for data packets of length 10 and for a number of 10 retransmissions. Of course, the approach cannot "prove" the correctness of the protocol for arbitrary lengths of the packets and/or an arbitrary number of retransmissions, but it provides a better understanding of the protocol's behaviour and a certain degree of confidence in its correctness. Moreover, model-checking has the advantage of being completely automated and efficient (we performed the above verifications in a few minutes). The whole case-study took approximately one week.

This protocol has also been studied in the framework of theorem-proving [Groote-vandePol-93,Helmink-Sellink-Vaandrager-94] and theorem-proving combined with model-checking [Havelund-Shankar-95]. It is worth noticing that, although some of these approaches allowed a complete correctness proof of the protocol, they required a much larger amount of manpower (several man-months).

As regards the specification formalism, we found LOTOS very adequate for this kind of application. The LOTOS descriptions we obtained are quite compact (4.5 pages of source code) compared to 11 pages of Murphi description language in [Havelund-Shankar-95]. The new standard E-LOTOS (Extended LOTOS), which is currently under work at ISO, should allow an even more concise description.

Publications: [Groote-vandePol-93] Jan Friso Groote and Jaco Van de Pol. "A bounded retransmission protocol for large data packets." Technical Report Logic Group Preprint Series 100, Utrecht University, October 1993.

[Havelund-Shankar-95] Klaus Havelund and Natarajan Shankar. "Experiments in Theorem Proving and Model Checking for Protocol Verification." In Marie-Claude Gaudel and Jim Woodcock, editors, Proceedings of the IFIP WG 14.3 3rd International Symposium of Formal Methods Europe FME'96 (Oxford, UK), Lecture Notes in Computer Science vol. 1051, pp. 662-681, March 1996.

[Helmink-Sellink-Vaandrager-94] L. Helmink, M. P. A. Sellink, and F. W. Vaandrager. "Proof-checking a data link protocol." In Proceedings of the 1st International Workshop on Types for Proofs and Programs, LNCS vol. 806, pp. 127-165, May 1993.

[Mateescu-96] Radu Mateescu. "Formal Description and Analysis of a Bounded Retransmission Protocol." In Zmago Brezocnik and Tatjana Kapus, editors, Proceedings of the COST 247 International Workshop on Applied Formal Methods in System Design (Maribor, Slovenia), University of Maribor, Slovenia, June 1996. Also available as INRIA Research Report RR-2965.
Available on-line from http://cadp.inria.fr/publications/Mateescu-96.html

[Mateescu-97] Radu Mateescu. "Vérification de systèmes répartis : l'exemple du protocole BRP." Technique et science informatiques 16(6):725-751, June 1997.
Contact:
Radu Mateescu
INRIA Rhône-Alpes / VASY
655, Avenue de l'Europe
38330 Montbonnot Saint Martin, FRANCE
Tel: +(33) 04 76 61 52 83
Fax: +(33) 04 76 61 52 52
e-mail: Radu.Mateescu@inria.fr



Further remarks: The LOTOS sources as well as explanations on the verification with CADP are available on line at : ftp://ftp.inrialpes.fr/pub/vasy/demos/demo_16

This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies


Last modified: Tue Sep 8 18:14:48 2015.


Back to the CADP case studies page