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 of the individual components present designers with unprecedented challenges in the areas of modularity and dependability. This paper describes two ideas regarding a modular approach to specifying and reasoning about mobile computing. The novelty of our approach rests with the notion of allowing transient interactions among programs which mobe in space. In this paper we restrict our concert to pariwise interactions involving variable sharing and action asynchronization. The motivation behind the transient nature of the interactions comes from the fact that components can communicate with each other only when they are within a certain range. The notation we propose is meant to simplify the writing of mobile applciaitons and is a direct extension of that used in UNITY. Reasoning about mobile bomputations relies on the UNITY proof logic.
Roman, Gruia-Catalin; McCann, Peter J.; and Plun, Jerome, "Assertional Reasoning about Pairwise Transient Interactions in Mobile Computing" Report Number: WUCS-95-26 (1995). All Computer Science and Engineering Research.