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:	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 the CADP Web site in PDF or PostScript
Contact:	Henri Korver CWI P.O. Box 94079 1090 GB Amsterdam The Netherlands E-mail: H.Korver@idr.nl
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