|
| 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: |
ALCATEL CIT (FRANCE)
|
|---|---|
| Method: |
LOTOS
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes)
|
| Domain: |
Telecommunications.
|
| Period: |
1994
|
| Size: |
|
| Description: |
The ISDN telephony teleservice and call waiting service were described
in LOTOS, using ITU's recommendations on ISDN. The specification was
written in a step by step approach, which enabled simulation before
every evolution.
The description was then adapted in order to enable verification with
CADP, which means avoiding state space explosion.
|
| Conclusions: |
This study showed the necessity of the verification of protocols and
services through their formal specification. The ITU recommendations,
by their ambiguity and their too static descriptions lead to studies
that are influenced by interpretation.
The tool support that is available for the LOTOS language is certainly a great reason to use this language, but they are limited by problems (State space explosion) which should be solved. |
| Publications: |
Eric Valade, Rapport de Tutorat ESSAT, Specification LOTOS et
Verification du service Telephonie RNIS et de l'appel en instance.
|
| 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