This paper presents a formal development of a Radio Telephone System by a sequence of correctness-preserving refinements. We follow several steps of refinement from an abstract applicative specification which is validated against the properties and behavior of a basic telephone service, to a specification involving a central station and a number of remote stations communicating synchronously by means of radio channels. Particular features of the development are the decomposition of the basic telephone service into separate layers for the phones and the communication network, and the introduction of finite communication resources. We verify that the decompositions preserve correctness and that the resources are allocated and released correctly. The work was carried out with the RAISE specification language and its associated method, using the RAISE tools.
