Abstract:

GSM (Global System for Mobile Communications) is a European standard for mobile (cellular) telephony. It was standardized by ETSI (European Telecommunications Standards Institute). It is a digital system which allows international roaming for its subscribers, has sophisticated security features, etc. LOTOS (Language Of Temporal Ordering Specification) is a formal specification language which is a ISO standard. Its aim is to allow abstract and precise definition of complex distributed systems. Because it is executable, LOTOS specifications constitute a `model' which can be exercised to see how the entity specified is supposed to work. Because it has formal semantics, LOTOS specifications can be the object of formal validation and verification. The three main layers of GSM were specified in LOTOS: Radio Resource Management, Mobility Management, and Communications Management. This is the whole of GSM with the exception of the Operation and Management Subsystem. The specification consists of about 3,000 lines of LOTOS. This experience has shown that LOTOS and existing LOTOS tool are well-suited to the task. We present the main philosophy of our specification approach and the main structural aspects of our specification.The specification can be used to document the standard, to help understand the standard, and as a basis for information exchange between implementors using different platforms. The main motivation of this exercise was to obtain `use cases' for GSM. Such use cases are useful in several ways:

• They can constitute an important documentation aspect of the standard, comparable to time-sequence diagrams.
• They can be used for the formal analysis of the specification. For example, by generating appropriate use cases it is possible to see whether security requirements are met.
• They can be used for the generation of test cases: in fact, test case generation can be automated to a certain extent by using our specification and appropriate tools.