Title :
Prototyping and formal requirement validation of GPRS: a mobile data packet radio service for GSM
Author :
Andriantsiferana, Laurent ; Ghribi, Brahim ; Logrippo, Luigi
Author_Institution :
Sch. of Inf. Technol. & Eng., Ottawa Univ., Ont., Canada
Abstract :
A methodology and an experience for validating a substantial part of a mobile data standard, ETSI´s General Packet Radio Service, is presented. The standard was specified in LOTOS, which provided a formal prototype for the system. Testing processes were composed with the specification, and temporal logic properties were checked. At least two major design errors were identified
Keywords :
cellular radio; formal specification; formal verification; packet radio networks; packet switching; specification languages; telecommunication computing; telecommunication standards; temporal logic; GPRS; GSM; General Packet Radio Service; LOTOS; design errors; formal requirement validation; mobile data packet radio service; mobile data standard; prototyping; temporal logic; testing; Formal specifications; GSM; Ground penetrating radar; Logic testing; Packet radio networks; Protocols; Prototypes; Software engineering; Software prototyping; Telecommunication standards;
Conference_Titel :
Dependable Computing for Critical Applications 7, 1999
Conference_Location :
San Jose, CA
Print_ISBN :
0-7695-0284-9
DOI :
10.1109/DCFTS.1999.814292
