Telecommunications Software Engineering Research Group,
School of Information Technology and Engineering, University of Ottawa
CADP (Construction and Analysis of Distributed Processes)
RTL (Real-Time LOTOS)
GSM (Global System for Mobile communications) is an European standard
for cellular communications delveloped by ETSI (European
Telecommunications Standard Institute). GPRS is a set of new GSM bearer
services that provide packet mode transmission within the GSM network
and inter-works with external packet data networks. GPRS is a full
digital system and is still an evolving standard that spans beyond
telephony and circuit switched services.
GPRS services are divided into two categories: Point-to-Point (PTP) and Point-to-Multipoint (PTM) services. Possible PTP services include: data base access and infomation retrieval; the Internet; messaging and conversational services from user to user; credit card validation, etc. PTM services include: unidirectional distribution of information such as news and weather reports; conferencing services between multiple users, etc.
A formal specification of GPRS has been written in LOTOS, covering the following functions: network access control, logical link management, packet routing and transfer, and mobility management. The abstract GPRS model considered is based on the following assumptions: the GPRS network is composed of four RAs (Routing Areas), each one having two cells; there are one SGSN (Serving GPRS Support Node) and one MSC/VLR (Mobile Switching Center/Visitor Location Register) for each pair of RAs; there is one HLR (Home Location Register) in the network; and two GGSNs (Gateway GPRS Support Node) serve as connections to the external networks.
The methodology adopted for validating the LOTOS specification combines concepts of testing and model-checking. Four test suites were identified (with a total of 35 tests), covering the following aspects: attach and detach procedures; PDP context activation and deactivation procedures; data delivery between MS and external network; routing update procedures and data delivery. The test processes were composed in parallel with the original LOTOS specification and the corresponding LTS models were generated using RTL and reduced using ALDEBARAN. For each test, the execution sequences leading to may pass results have been extracted using EXHIBITOR and examined by translating them into MSCs (Message Sequence Charts).
Starting from the captured requirements of GPRS, a set of (over 20) correctness properties were identified. These properties have been expressed formally as modal mu-calculus formulas and verified on the LOTOS specification of GPRS using the EVALUATOR model-checker.
Several specification problems were detected using these validation techniques. The two main ones concern: Mobility Management state conflicts (packets that cannot be forwarded properly fo the MS); and routing updates and data delivery conflicts (loss of data).
This case-study makes use of formal methods for the verification of
crucial properties of the GPRS forthcoming standard. The application
of the validating methodology to this complex system required a lot
of ingenuity, both in developing the specification and in making the
tools work towards the goals.
At least two significant design errors have been found. Each one of them, if not addressed, would have led to faulty functioning of the system, possibly involving loss of data or of connectivity to the mobile user. This experience confirms the usefulness of formal methods in the design of dependable critical systems.
L. Logrippo and L. Andriantsiferana and B. Ghribi.
"Prototyping and Formal Requirement Validation of GPRS: A Mobile
Data Packet Radio Service for GSM". Proceedings of the 7th IFIP
International Working Conference on Dependable Computing for Critical
Applications DCCA-7 (San Jose, California, USA), January 1999.
Available online at: http://LOTOS.csi.UOttawa.ca/ftp/pub/Lotos/Papers/dcca7.ps.gz
or also from the CADP Web site in PDF or PostScript
Prof. Luigi Logrippo
School of Information Technology and Engineering
University of Ottawa
150 Louis Pasteur
P.O. Box 450 Stn A
Ottawa Ontario Canada
Tel: (613) 562-5800 x 6704
Fax: (613) 562-5187 or (613) 562-5185
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|