Formal Specification and Validation using a Scenario-Based Approach:
The GPRS Group-Call Example

D. Amyot, N. Hart, L. Logrippo, and P. Forhan

Abstract

This paper applies the UCM-LOTOS design/validation approach to an example
taken from mobile telephony: GSM's General Packet Radio Services. It
also discusses relationships between UCMs, LOTOS and ROOM.