DocumentCode
3445260
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
fYear
1999
fDate
36465
Firstpage
109
Lastpage
128
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Dependable Computing for Critical Applications 7, 1999
Conference_Location
San Jose, CA
Print_ISBN
0-7695-0284-9
Type
conf
DOI
10.1109/DCFTS.1999.814292
Filename
814292
Link To Document