Database of Case Studies Achieved Using CADP

Verification of an ATM Switch

Organisation: ENST Paris (France)

Method: LOTOS

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

Domain: Network systems.

Period: 1994

Size: n/a

Description: ATM is a switching and multiplexing technique, selected by ITU for broadband ISDN. An ATM switching fabric, inspired from the Batcher Banyan multistage interconnection network, has been specified in LOTOS. The five functions of the fabric (filter, routing table, batcher, trap and Banyan) are reflected as five concurrent components in the specification. An abstract monolithic specification of the intended behaviour has also been written. Both versions describe a 2x2 switch. CAESAR has been used to produce models for the two specifications, which have been proved (observationally) equivalent using ALDEBARAN. A model for a 4x4 Banyan has also been produced and verified, by showing that no erroneous state is reachable (internal contention or incorrect routing).

Conclusions: Because of the parallelism concept and the underlying notion of synchronism, LOTOS appears to be more appropriate for this specification than other languages like Estelle or SDL. The extension of our approach to a NxN switch is straightforward, and remains applicable if a small change was made on the specification, whereas a more mathematical proof would have to be redone in whole.

Publications: A. Février, E. Najm, N. Prost, F. Robles, Verifying an ATM Switch with Formal Methods, 4th Open Workshop on High Speed Network. Available on-line from our FTP site in PDF or PostScript
Arnaud Février
Laboratoire d'Informatique de Marseille
Tel: +33 4 91 17 79 26


Elie Najm
ENST Paris
Département Réseaux
46, rue Barrault
75013 Paris
Tel: +33 1 45 81 77 09
Fax: +33 1 45 89 16 64

Further remarks: This case study, amongst others, is described on the CADP Web site:

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

Back to the CADP case studies page