Department of Software Technology, CWI Amsterdam (THE NETHERLANDS)
Computer Science Laboratory, Ericsson Stockholm (SWEDEN)
muCRL (micro Common Representation Language)
CADP (Construction and Analysis of Distributed Processes)
about 1600 lines of muCRL
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.
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.
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
I.A. van Langevelde
P.O. Box 94079
NL-1090 GB Amsterdam
Tel: +31 20 592 4165
Fax: +31 20 592 4199
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|