Database of Case Studies Achieved Using CADP

GSM Handover Procedure

Organisation: Swedish Institue of Computer Science

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Telephony.

Period: 1990-1991

Size: 7000 states

Description: The Public Land Mobile Network (PLMN) proposed by the European Telecommunication Standards Institute (ETSI) is a cellular system composed of mobile stations, base stations, mobile switching centres, and a location register. Mobile stations provide communication services to an end-user. Base stations manage radio communications in a fixed geographic area, called cell: all communication with mobile stations in a cell is routed through the base station responsible for the cell. A mobile switching center manages a set of base stations. Location registers store the information in which cell a mobile station can be found.

This case study focusses on the handover procedure, which governs the movement of a mobile station from one cell to another, including the modification of the radio communication links and the update of the location register. To specify the handover procedure in LOTOS, the dynamic communication structure is encoded in the data part, using offers to distinguish between synchronizations on a common gate.

The corresponding LOTOS specification is generic and can be instantiated for various numbers of mobile stations, base stations, radio channels, and mobile service centers. Besides a detailed specification of the handover procedure, also an abstract service involving only the gates visible from the outside has been specified.

For each specification, the corresponding LTS (Labeled Transition System) was generated (using the CAESAR.ADT and CAESAR tools) and minimized for strong bisimulation (using the ALDEBARAN tool). These steps were possible for configurations with up to two mobile stations and three base stations with a radio channel each (7,000 states).

Conclusions: Encoding communication link names as LOTOS data values enables the verification of dynamic systems, the communication structure of which respects certain conditions. In this case, the GSM handover procedure could be proven observational equivalent to an abstracter service description.

Publications: [Fredlund-Orava-91] Lars-Åke Fredlund and Fredrik Orava. "Modelling Dynamic Communication Structures in LOTOS". Proceedings of the 4th International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols FORTE'91 (Sydney, Australia), pp. 185-200, North-Holland, 1992.
Available on-line at:

Lars-Åke Fredlund
Swedish Institute of Computer Science
Box 1263
S-164 28 Kista

Further remarks: This case-study, amongst others, is described on the CADP Web site:

Last modified: Mon Jul 4 11:04:00 2022.

Back to the CADP case studies page