next up previous

Final Report of the COST-247 Action

Formal Specification and Generation of Use Cases for a Mobile Telephony Standard

Luigi Logrippo, Amine Rachdi, Randy Tuok

Protocols Research Group
Computer Science Department
University of Ottawa
Ottawa, Ontario
Canada K1N 6N5
Tel: (613)-564-5450
Fax: (613)-564-9486


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:

In current industrial practice, use cases are generated by hand on the basis of informal specifications. The use of LOTOS and LOTOS methodology simplifies the creation and maintenance of use cases. We describe the methods and tools that were applied to generate automatically GSM use case from the LOTOS specification. Tools used include Ottawa's ELUDO, Grenoble's CAESAR/ALDEBARAN, and Madrid's LOLA.

This presentation has been given during the COST-247 4th Management Committee Meeting (Berlin, Germany, February 9--10, 1995).

COST-247 Working Group(s): 1

This Page was prepared by Mark Jorgensen.

Back to the VASY Home page