Database of Case Studies Achieved Using CADP

Alternating Bit Protocol

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 our FTP 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:
ftp://ftp.inrialpes.fr/pub/vasy/demos/demo_02

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


Last modified: Fri Feb 19 09:12:04 2016.


Back to the CADP case studies page