TCAP Protocol (Transaction Capabilities Procedures).

Organisation:	Department of Software Technology, CWI Amsterdam (THE NETHERLANDS) Computer Science Laboratory, Ericsson Stockholm (SWEDEN)
Method:	muCRL (micro Common Representation Language)
Tools used:	muCRL toolset CADP (Construction and Analysis of Distributed Processes)
Domain:	Communication Protocols.
Period:	1999.
Size:	about 1600 lines of muCRL
Description:	TCAP (Transaction Capabilities Procedures) is a protocol for the deployment of advanced "intelligent" services over a telecommunication network. Examples of services delivered by TCAP are routing associated with toll-free numbers, checking personal identification of calling users, and authentication, equipment identification and roaming of GSM phone users. An optimisation of the TCAP protocol became possible when it moved from a multi-processor architecture to a single-processor architecture. A smart redesign provided an optimised version of TCAP, but the question as to what extent this version covered the functionalities required, remained open. A formal approach was chosen for describing and comparing the two versions of the protocol. Both the original and the optimised versions of TCAP have been formally described in muCRL, by translating the original SDL and ERLANG specifications. This effort alone allowed to detect and correct several minor mistakes in the original specification, but also an important bug in the optimised version of TCAP (a local message caught in a wrong state). The external environment of TCAP in the muCRL specification was refined and the communication media were restricted to one-datum buffers in order to obtain finite-state specifications. The LTS models of the two specifications have been generated using the muCRL toolset. These LTSs were inspected using the graphical tools BCG_DRAW and BCG_EDIT, and compared using ALDEBARAN. Several differences between the two models, concerning non-determinism and concurrency, have been detected. Some of them were identified as potential bugs (e.g., the order of garbage collecting and process killing actions), while some others appeared to be harmless but had to be carefully isolated and explained.
Conclusions:	This case-study was successful in that it traced several bugs in the TCAP specification and proposed a fix for each, thus constructively contributing to an improved optimised redesign of the protocol. The method of bisimulation checking, the specification language muCRL, and the muCRL and CADP toolsets proved to be sufficiently powerful to support the verification of TCAP. The verification process turned out to be a non-trivial task rather than a routine computerised check. It required both a deep understanding of the TCAP protocol and an expertise in using specification languages and verification tools.
Publications:	[ITU-93] International Telecommunication Union. "Signalling System No. 7 - Transaction Capabilities Procedures". Edition 03/93, march 1993. [Arts-Langevelde-99-a] Thomas Arts and Izak van Langevelde. "How muCRL Supported a Smart Redesign of a Real-life Protocol". In Stefania Gnesi and Diego Latella, editors, Proceedings of the 4th International ERCIM Workshop on Formal Methods for Industrial Critical Systems (Trento, Italy), pages 31-53, ERCIM, CNR, July 1999. [Arts-Langevelde-99-b] Thomas Arts and Izak van Langevelde. "Verifying a smart design of TCAP; A synergetic experience". Technical Report SEN-R9910, CWI, Amsterdam, April 1999. Available on-line at: http://www.cwi.nl/static/publications/reports/abs/SEN-R9910.html or also from the CADP Web site in PDF or PostScript [Arts-Langevelde-01] Thomas Arts and Izak van Langevelde. "Correct Performance of Transaction Capabilities". In Proceedings of the 2nd International Conference on Application of Concurrency to System Design ICACSD'2001 (Newcastle upon Tyne, UK), pp.35-42, IEEE Computer Society, June 2001. Available on-line at: ftp://ftp.cwi.nl/pub/izak/papers/icacsd01.pdf" or from the CADP Web site in PDF or PostScript
Contact:	I.A. van Langevelde CWI Kruislaan 413 P.O. Box 94079 NL-1090 GB Amsterdam The Netherlands Tel: +31 20 592 4165 Fax: +31 20 592 4199 E-mail: Izak.van.Langevelde@cwi.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