Document Type

Technical Report

Department

Computer Science and Engineering

Publication Date

1995-01-01

Filename

WUCS-95-01.PDF

DOI:

10.7936/K7RJ4GQ9

Technical Report Number

WUCS-95-01

Abstract

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. This paper describes a modular approach to specifying and reasoning about of mobile computing. Its novelty rests with the notion of allowing transient (location-dependent) data sharing among programs which move in space. The notation is a direct extension of that used in UNITY and reasoning about mobile computations relies on the UNITY proof logic. Several examples explain the notation, demonstrate the modularity of the approach, and illustrate the verification methodology. An electronic-mail distribution problem is presented in some detail.

Comments

Permanent URL: http://dx.doi.org/10.7936/K7RJ4GQ9

Download

Share

COinS