General Packet Radio Service (GPRS).

Organisation:	Telecommunications Software Engineering Research Group, School of Information Technology and Engineering, University of Ottawa (CANADA)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes) RTL (Real-Time LOTOS)
Domain:	Mobile Telephony.
Period:	1998-1999.
Size:
Description:	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).
Conclusions:	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.
Publications:	[Andriantsiferana-Ghribi-Logrippo-99] 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
Contact:	Prof. Luigi Logrippo School of Information Technology and Engineering University of Ottawa 150 Louis Pasteur P.O. Box 450 Stn A Ottawa Ontario Canada K1N 6N5 Tel: (613) 562-5800 x 6704 Fax: (613) 562-5187 or (613) 562-5185 E-mail: luigi@site.uottawa.ca
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