Abstract
This paper presents the results of experimentation performed on the application of a specification language and three conformance testing techniques to the validation of the gsm-map protocol (Global System for Mobile communication - Mobile Application Part). The gsm-map protocol is a component of the GSM radiocommunication system that describes the signaling functions required in signaling system SS7 to offer the services needed in a mobile network. The etsi standard describes this protocol in a semiformal way that we have formalized (using the sdl formal language), to improve its testability. We have then applied three different testing techniques : embedded testing techniques to perform the test of functional components embedded in the global system, global testing techniques to test the complete protocol and passive testing techniques to verify whether the protocol execution traces are accepted or not by the specification (represented by a finite state machine or by an extended finite state machine).
Résumé
Le protocole gsm-map (Global System for Mobile communication - Mobile Application Part) est un composant du système de radiocommunication GSM. Ce protocole décrit les fonctions de signalisation nécessaires dans le système de signalisation SS7 pour offrir aux utilisateurs les services demandés dans un réseau mobile. Cet article présente les résultats expérimentaux obtenus pour la validation de ce protocole de communication mobile, le protocole gsm-map. Ces recherches ont été réalisées en utilisant un langage formel de spécification et par l’application de trois méthodes différentes de test. La spécification quasi-formelle décrite dans la norme etsi du protocole gsm-map) est formalisé en lds (langage de description et de spécification). Un composant imbriqué du protocole (le processus map-requesting-ssm) dans le contexte d’un autre composant du protocole (le processus map-dsm) est testé, c’est-à-dire que l’on effectue le test imbriqué d’un composant qui ne pouvait pas être directement accédé par le testeur. La deuxième méthode de test appliquée a pour but le test complet du comportement global du système et a été possible par l’introduction d’une nouvelle approche de modélisation en lds des procédures. L’approche de traitement des procédures a été validée par une troisième méthode de test : le test passif. Cette dernière technique de test vérifie si les traces d’exécution (appartenant au comportement du protocole) sont acceptées ou non par sa spécification (représentée comme une machine à états finis ou comme machine à états finis étendue).
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Clatin (M.), Groz (R.), Phalippou (M.), Thummel (R.). Two approaches linking a test generation tool with verification techniques. In A. Cavalli and S. Budkowski editors,Proceedings of iwpts’95 (8th Int. Workshop on Protocol Test Systems, INT, Évry, France, (September 1995).
Fernandez (J. -C),Jard (C),Jeron (T.),Viho (C). An experiment in automatic generation of test Suites for protocols with verification technology.Science of Computer Programming,29, (1997).
Grabowski (J.),Hogrefe (D.),Scheurerand (R.),Dai (Z. R.). Applying samstag to the b-isdn Protocol sscop. In M. Kim, S. Kang and K. Hong editors.Proceedings of iwcts’97 (10th Int. Workshop on Testing of Communicating Systems, Korea), (September 1997).
***Cinderella sdl product description, http :// www.cinderella.dk
Bourhfir (C),Dssouli (R.),Aboulhamid (E. M.),Rico (N.). A test case generation tool for conformance testing of sdl systems. In R. Dssouli, G. V. Bochmann and Y. Lahav editors,Proceedings of SDL ’99, Elsevier, (June 1999).
Besse (C),Cavalli (A.),Lee (D.). An automatic and optimized test generation technique applying to tcp/ip protocol.Proceedings of the 14th IEEE International Conference on Automated Software Engineering (ase’99). Cocoa Beach, Florida, (12-15 October 1999).
Lima (L. P.),Cavalli (A.). A pragmatic approach to generating test sequences for embedded systems.Proceedings of jwcrs’97 (10th Int. Workshop on Testing of Communicating Systems,Korea), pp. 125-140, (September 1997).
Lima (L. P.). Une méthode pragmatique de génération de séquences de test pour les systèmes imbriqués.PhD thesis. Université d’Évry, France, (Novembre 1998).
Tabourier (M.),Cavalli (A.),Ionescu (M.). A gsm-map proto- col experiment using passive testing,fm’99 World Congress on Formal Methods in the Developement of Computing Systems, Toulouse, France, (20-24 September 1999).
*** Specification and description language,ccmz.100, International Consultative Committee on Telegraphy and Telephony, Genève, (1992).
*** Digital cellular telecommunication system (Phase2+); mobile application part (MAP)etsi specification, (gsm 09.02), (August 1996).
*** Verilog, objectGEODE sdl Editor -User’s Guide, France, (1997).
Aho (A.),Dabhura (A.),Lee (D.),Uyar (U.). An optimization technique for protocol conformance test generation based on UIO sequences and rural Chinese Postman Tours,pstv’88, S. Aggar- wal and K. Sabnani (Editors), North Holland, pp. 75-86, (1988).
Cavalli (A.), Chin (B. M.), Chon (K.). Testing methods for sdl systems.Computer Networks and isdn Systems,28, pp. 1669–1683,(1996).
Sidhu (D. P.), Leung (T. K.). Formal methods for protocol testing : a detailed study.IEEE Transaction on Software Engineering,15, n° 4, (April 1989).
***Verilog, objectGEODE sdl simulator-getting started, France, (1997).
Aho (A.),Sethi (R.),Ulman (J.). Compilers, principles, techniques and tools.Addison-Wesley Publishing Company, (1986).
Chen (M. S.),Choi (Y.),Kershenbaum (A.). Approaches utilizing segment overlap to minimize test sequences,pstv’90, pp. 67–84, Canada, (June 1990).
Anido (R.),Cavalli (A.),Lima (L. P.),Clatin (M),Phalippou (M.). Engendrer des tests pour un vrai protocole grâce à des tech niques éprouvées de vérification.Proceedings of cfip’96 - Rabat, Maroc, (14–17 October 1996).
Lima (L. P.),Cavalli (A.). Service validation - an embedded testing approach.Proceedings of Eunice Summer School, Lausanne, Switzerland, (23–27 June 1996).
***iso, Information technology, open systems interconnection, conformance testing methodology and framework,International Standard IS-9646, (1991).
Lima (L. P.),Cavalli (A.). Application of embedded testing methods to service validation.2nd IEEE Intern. Conf. On Formal Engineering Methods, Brisbane, Australia, (1998).
Ionescu (M.),Cavalli (A.). Test imbriqué du protocole map- GSM.Proceedings of Colloque Francophone sur l’Ingénierie des Protocoles CFIP’99, Nancy, France, (26-29 April 1999).
Scitz (C. L.). An approach to designing checking experiments based on a dynamic model.In Theory of Machines and Computations, Z.Kohavi and A. Paz Ed., Academic Press, (1972).
Lee (D.) et al., Passive testing and applications to network management.icnp ’97 International Conference on Network Protocols, Atlanta, Georgia, (October 28-31, 1997).
Lagrange (X.),Godlewski (P.),Tabbane (S.). Réseaux gsm- dcs - des principes à la norme.Hermès Éditions, Paris, (1995).
Charbonnier (A.),Hartmann (C),Thomas (R.). Les architectures des réseaux mobiles, Le Conseil scientifique de France Télécom,Memento technique number 9. Architecture des réseaux de télécommunications, cnet, (June 1997).
Janssen (U.),Nielsen (B.). The map for gsm phase 2.mrc Mobile Conference, see, Vulpine, France, (1991).
*** Message sequence chart (msc).itu-t Rec Z.120, Geneva, (1996).
***Tekelec,CCS7/MGTS User’s Manual, P/N 910-1498-01, Revision A, (September 1997), http://tekelec.fr
Author information
Authors and Affiliations
Corresponding authors
Rights and permissions
About this article
Cite this article
CAVALLI, A., Ionescu, M. Validation of the GSM-map protocol. Ann. Télécommun. 55, 58–69 (2000). https://doi.org/10.1007/BF02997772
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF02997772
Key words
- Mobile radiocommunication
- GSM
- Communication protocol
- Validation
- Formal description technique
- Specification language
- lds
- Conformance testing
- Finite automation
- Test generation