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 |
E-mail: luigi@csi.uottawa.ca |
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:
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.