Database of Case Studies Achieved Using CADP

Feature Interactions in Telephony Systems.

Organisation: CWI (The Netherlands)

Method: LOTOS

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

Domain: Telecommunications.

Period: 1996

Size: 360 lines of LOTOS

Description: The study centers around a LOTOS description of two telephone services Abbreviated Dialling (ABD) and Originating Call Screening (OCS). Bouma and Zuidweg (Dutch PTT) formalised a simple example of feature interaction between these two services: if a dialled number is expanded too late, it might not be recognised as belonging to the list of numbers to be screened. Bouma & Zuidweg's work has been extended by the use of the CADP verification tools.
The verification was done by observing the graphs generated from the specification, and features were checked with testers. A tester is a simple LOTOS description which encodes a property to be checked and runs in parallel with the original specification. As soon as the property to be tested is violated, the tester fires a special error transition. These testers were used to discover errors and to prove positive properties.

Conclusions: This experiment is successful: the results of Bouma and Zuidweg are strengthened by the application of verification tools. In particular a bug was found in the model. To repair the error, the implementation of the ABD service had to be changed.

Publications: Henri Korver, Detecting Feature Interactions with CAESAR/ALDEBARAN, W. Bouma and H. Zuidweg. Formal Analysis of feature interactions by model checking. Proceedings of the Second Workshop on Protocol Verification, Eindhoven, The Netherlands, 1993

Henri Korver, Detecting Feature Interactions with CAESAR/ALDEBARAN, Science of Computer Programming, special issue on Industrially relevant Applications of Formal Analysis Techniques, J.F. Groote and M. Ren, editors, July 1997.
Available on-line from our FTP site in PDF or PostScript
Henri Korver
P.O. Box 94079
1090 GB Amsterdam
The Netherlands

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