|
| 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: |
LGI/IMAG (Grenoble, France)
|
|---|---|
| Method: |
LOTOS
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
|
| Domain: |
Networks
|
| Period: |
1989
|
| Size: |
266 lines of LOTOS
up to 520,000 states and 1,700,000 transitions |
| Description: |
The alternating bit protocol belongs to the transport layer (4th layer of the OSI
model) and implements a reliable transmission service above unreliable
communication media.
The protocol was described as a set of four concurrent LOTOS processes: a transmitter, a receiver, and two communication media that can either reliably transmit messages and acknowledgements, or lose them with explicit loss indication, or lose them silently. The specification is parameterized by the number N of different messages that can be sent by the transmitter. The verification was carried out by generating (using CAESAR) the labelled transition system corresponding to the alternating bit protocol for each value of N in {5, 10, 15, 20, 25, 30, 35, 40, 45, 50, 70}, and showing (using ALDEBARAN) observational equivalence with the labelled transition system describing the expected service (i.e., a simple automaton expressing that each message being sent by the transmitter is duly got by the receiver). |
| Conclusions: |
This case study was truly the first one performed by jointly using the CAESAR
and ALDEBARAN tools, the combination of which gave birth to the CADP toolbox.
Taking the alternating bit protocol as a example, the study demonstrated that model-based verification (namely, state space exploration and equivalence checking) was tractable for descriptions written in a process calculus such as LOTOS, in contrast with approaches based on symbolic simulation and theorem proving that had been predominating so far. |
| Publications: |
[Garavel-89-b-CD]
Hubert Garavel.
"Utilisation de CAESAR et ALDEBARAN".
Technical report, 24 pages, in French.
Based on Appendix C of Hubert Garavel's PhD thesis "Compilation et vérification de programmes LOTOS", Thèse de Doctorat, Université Joseph Fourier (Grenoble), November 1989. http://cadp.inria.fr/publications/Garavel-89-b.html Available on-line from: http://cadp.inria.fr/publications/Garavel-89-b-CD.html or from the CADP Web site in PDF 
or
PostScript 
|
| Contact: | Hubert Garavel LGI - IMAG Campus BP 53X 38041 GRENOBLE cedex FRANCE |
| Further remarks: |
The LOTOS descriptions as well as explanations on the verification with
CADP are available on-line at: http://cadp.inria.fr/ftp/demos/demo_02 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