|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools Forum |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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: https://doi.org/10.1016/B978-0-444-89402-1.50023-0 |
| Contact: | Lars-Åke Fredlund Swedish Institute of Computer Science Box 1263 S-164 28 Kista SWEDEN Email: fred@sics.se |
| 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