Prototyping and Formal Requirement Validation of GPRS:
A Mobile Data Packet Radio Service for GSM

Laurent Andriantsiferana, Brahim Ghribi, Luigi Logrippo
University of Ottawa

Abstract

A methodology and an experience for validating a substantial part
of a mobile data standard, ETSIs 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.