|
| 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 Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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 the CADP Web site in
PDF 
or
PostScript 
|
| Contact: | Arnaud Février Laboratoire d'Informatique de Marseille Tel: +33 4 91 17 79 26 E-mail: fevrier@lim.univ-mrs.fr or: Elie Najm ENST Paris Département Réseaux 46, rue Barrault 75013 Paris FRANCE Tel: +33 1 45 81 77 09 Fax: +33 1 45 89 16 64 E-mail: najm@res.enst.fr |
| Further remarks: | 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