Mobile UNITY coordination constructs applied to packet forwarding for mobile hosts

With recent advances in wireless communication technology, mobile computing is an increasingly important area of research. A mobile system is one where independently executing components may migrate through some space during the course of the computation, and where the pattern of connectivity among the components changes as they move in and out of proximity. Mobile UNITY is a language and logic for specifying and reasoning about mobile systems, the components of which must operate in a highly decoupled way. In this paper it is argued that Mobile UNITY contributes to the modular development of system specifications precisely because of the decoupled and declarative fashion in which coordination among components is specified. The packet forwarding mechanism which is at the core of the Mobile IP protocol for routing to mobile hosts is taken as an example. A Mobile UNITY specification of packet forwarding and the mobile system in which it must operate is developed. Mobile hosts are the components that can disconnect from one location in the network and reconnect to another at any point during system execution. Finally, the role of formal program verification in the development of protocols like Mobile IP is discussed.