An algebraic verification of a mobile network

Abstract

In a mobile communication network some nodes change locations, and are therefore connected to different other nodes at different points in time. We show how some important aspects of such a network can be formally defined and verified using the π -calculus, which is a development of CCS (Calculus of Communicating Systems) allowing port names to be sent as parameters in communication events. As an example of a mobile network we consider the Public Land Mobile Network currently being developed by the European Telecommunication Standards Institute and concentrate on the handover procedure which controls the dynamic topology of the network.