|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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 :
http://cadp.inria.fr/ftp/demos/demo_16
This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page