ALCATEL CIT (FRANCE)
CADP (Construction and Analysis of Distributed Processes)
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
The description was then adapted in order to enable verification with
CADP, which means avoiding state space explosion.
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.
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|