Validating Complex Telecommunication Software

by Sergio Contreras, María del Mar Gallardo, Pedro Merino, David Sanán, Javier Rivas and Joaquín Torrecilla

In a collaboration with the telecommunication company Centro de Tecnología de las Comunicaciones, S.A. (CETECOM), a research group at University of Malaga is validating communication software written in languages such as SDL, ASN.1 and C.

Automatic validation of many critical systems has usually been done with model-oriented techniques, like model checking. This approach requires the previous construction of a specific model (an abstraction) of the problem, using very specific languages oriented to academic tools like SPIN. In general terms, however, this abstraction is not well suited to automatically obtain an implementation. This is why this model-based methodology has only limited success within industry and is not generally employed, in particular, by telecommunication companies.

Many companies employ classic C and C++ languages for their critical communication software, and they have traditionally replaced validation by testing and/or debugging. Other companies use development languages that preserve validation facilities, as long as they are also powerful enough to automatically obtain the final software. In particular, they use standard description languages like the notations SDL (Specification and Description Language) and ASN.1 (Abstract Syntax Notation One), which are promoted by ITU-T (Telecommuni-cation Standardization Sector of the International Telecommunication Union). These languages offer an acceptable formal basis and they are linked to other standard notations, like TTCN (Tree and Tabular Combined Notation) and UML. In theory, using ITU-T languages makes it possible to perform validation at the same time that the software is developed; note that the executable code is obtained automatically by translating SDL to C/C++. However, these validation facilities seem to be under-exploited, and more efforts should be devoted to obtaining a methodology for effective validation of telecommunication software. This is one of the objectives of a joint project of the company Centro de Tecnología de las Comunicaciones, S.A. (CETECOM), the research institute Centro Andaluz de Innovación y Tecnología de la Información y las Comunicaciones (CITIC) and the Software Engineering Group of the University of Malaga (GISUM).

In particular, in the context of the project, CETECOM and GISUM are working on a methodology to validate existing complex software, using UMTS signalling as a case study. This software is mainly based on SDL to implement the protocol state machines, ASN.1 to describe the message types (as defined by standardization committees) and C to implement critical parts (like encoding/decoding algorithms). The whole software was produced with the tool Telelogic Tau. It contains more than 100,000 SDL symbols and it produces an implementation with more than 800,000 lines of C code. It is worth noting that such software has been previously tested with traditional methods and that it is complex enough to have Tau validation tool running for hours.

As expected, the first problem in performing validation is the size of the system. It produces millions of global states each having more than 20 Kbytes, considering only the SDL structures. However, there is a second more interesting problem. As current implementation is only a part of the whole signalling system, we need to complete the SDL description with information from the environment. The Tau validator can automatically produce many messages simulating the environment; realistic messages, however, have a great number of parameters that cannot be efficiently produced by the tools.

Validating with Tau: SDL diagram (left), validation script (center) and validation results (right).

We have designed a methodology to deal with both problems at the same time. The approach is based on the partitioning method proposed in the literature, but we have adapted it to existing heterogeneous software (SDL, ASN.1 and C). We isolate processes and blocks and construct a realistic environment for each partition. The environment is constructed as a validation script that limits the set of messages and the range of values in the messages. Then, the validator uses its internal mechanism to generate messages automatically.

Using validation scripts, we can perform validation of separate parts; however, we still need more optimization methods to deal with complexity. One of them is bitstate respresentation. Another one is variable hiding, which is applied to big C structures.

The project has been successful in terms of quality of the validation results (including the confirmation of the robustness of the code) and also in terms of the methodology generated. The work has also been useful to propose some extensions in the validation tool. We have shown that validation is a valuable task for existing telecommunication code, even when validation was not a primary aim during development. This is made possible by the use of standard languages like SDL with tool support.

Links:
CETECOM: http://www.cetecom.es
CITIC: http://www.citic.es
GISUM: http://www.lcc.uma.es/~gisum/

Please contact:
Maria del Mar Gallardo
University of Málaga/SpaRCIM, Spain
E-mail: gallardolcc.uma.es

Pedro Merino
University of Málaga/SpaRCIM, Spain
E-mail: pedrolcc.uma.es

Joaquín Torrecilla, CETECOM, Spain,
E-mail: jtorrecillacetecom.es