Document Type

Technical Report


Computer Science and Engineering

Publication Date






Technical Report Number



Mobile computing represents a major point of departure from the traditional distributed computing paradigm. The potentially very large number of independent computing units, a decoupled computing style, frequent disconnections, continuous position changes, and the location-dependent nature of the behavior and communication patterns present designers with unprecedented challenges in the areas of modularity and dependability. So far, the literature on mobile computing is dominated by concerns having to do with the development of protocols and services. This paper complements this perspective by considering the nature of the underlying formal models that will enable us to specify and reason about such computations. The basic research goal is to characterize fundamental issues facing mobile computing. We want to achieve this in a manner analogous to the way concepts such as shared variables and message passing help us understand distributed computing. The pragmatic objective is to develop techniques that facilitate the verification and design of dependable mobile systems. Towards this goal we employ the methods of UNITY. To focus on what is essential we center our study on ad-hoc networks whose singular nature is bound to reveal the ultimate impact of movement on the way one computes and communicates in a mobile environment. To understand interactions we start with the UNITY concepts of union and superposition and consider direct generalization to transient interactions. The motivation behind the transient nature of the interactinos comes from the fact that components can communicate with each other only when they are within a certain range. The notation we employ is a highly-modular extension of the UNITY programming notation. Reasoning about mobile computation relies on extensions to the UNITY proof logic.


Permanent URL: