Database of Case Studies Achieved Using CADP

ISDN telephony teleservice and call waiting

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


Last modified: Thu Jul 17 15:55:41 2014.


Back to the CADP case studies page