Derivation of an Algorithm for Location Management for Mobile Communication Devices
Beverly A. Sanders, Berna L. Massingill, Svetlana A. Kryukova · Parallel Processing Letters · 1998
In a network supporting mobile communication devices, a mechanism to find the location of a device, wherever it may be, is needed. In this paper, we present a distributed algorithm for this purpose along with its formal specification and proof sketch. Starting with an algorithm due to Wang, the process of formalization together with careful attention to abstraction leads to a more regular, general, and robust algorithm with a clearer description. An incidental contribution is a useful theorem for proving progress properties in distributed algorithms that use tokens.