Formal Treatment of Mobility. Our research group has been in the forefront of efforts to apply formal design techniques to mobile computing. Sometime in the early nineties, we asked ourselves whether UNITY style specification and refinement could be applied in a straightforward manner to the design of mobile systems. It was this investigation that ultimately resulted in the development of Mobile UNITY. In Mobile UNITY the description of a system is separated into mobile programs and interactions. Programs represent the basic units of mobility. They are described using a notation that closely resembles UNITY, all their variables are presumed to be local (at first sight), and each program includes a distinguished variable denoting its location in some logical or physical space. Mobile UNITY uses the location variable to capture movement. Access patterns to the location variable allow one to differentiate among programs that are oblivious to location changes, those that are aware of their current location, and those that control their own movement. By modeling movement as value assignment, the existing UNITY proof logic easily accommodates reasoning about space and motion. Interactions among mobile units are captured using a minimalist coordination language whose constructs allow one to specify asynchronous data transfer, reactive processing, and statement inhibition. The expressive power of the coordination language is derived from the constructs' ability to access variables, including location information, across program boundaries. To evaluate the expressive power of Mobile UNITY, we showed how these constructs are able to express low-level communication protocols (e.g., serial interfaces), novel high-level coordination constructs (e.g., transiently shared variables and transient statement synchronizations across mobile units), and clock synchronization. Most importantly, we extended the UNITY proof logic to accommodate the new constructs and the desired coordination semantics.

Reasoning about Code Mobility. In a separate case study we explored the applicability of the Mobile UNITY constructs to mobile code. We investigated a single application and compared design solutions that employed various mobile code paradigms, including remote evaluation, code on demand, and mobile agents. The study showed that the constructs of Mobile UNITY, particularly the specification and proof logic, apply to the area of logical mobility. Our foray into code mobility also led to the development of a fine-grained model of code mobility (CodeWeave). The first of its kind, this model allows for the movement of single variables, single statements, or complex block structured programs to locations on other hosts or even at points within other code fragments.

Mobile Protocol Verification. In an effort to show that Mobile UNITY provides meaningful abstractions for real problems in mobility, we used Mobile UNITY to specify and prove the correctness of Mobile IP, a protocol designed to facilitate the delivery of packets over the Internet to hosts that change the point of connection. We exploited the modular nature of Mobile UNITY by separately specifying the network, mobile agent, home agent, and foreign agent. The interactions section succinctly captured the synchronization and data sharing for the components, including the real-time constraint on the bounded clock drift between a mobile agent and its home agent. The formal verification of the protocol provided insights into how common informal notions of correctness relate to the conditions and assumptions under which the protocol is expected to behave properly.

Formal Perspective on Context Awareness. Context-aware computing refers to a computing paradigm in which the behavior of individual components is determined by the circumstances in which they find themselves to an extent that greatly exceeds the typical system/environment interaction patterns common to modern software systems. The environment has an exceedingly powerful impact on a particular application component either because the latter needs to adapt in response to changing external conditions or because it relies on resources whose availability is subject to continuous change. Built upon the Mobile UNITY notation and proof logic, Context UNITY is the first formal model intended to explicitly capture context-aware behaviors and it was part of an effort to develop a systematic understanding of the quintessential nature of context-aware computing. Starting with the basic premise that, in its most extreme form, context should be made manifest in a manner that is highly local in appearance and decoupled in fact, Context UNITY assumes a notion of context that is relative to the needs of each individual component and seeks to render the maintenance of contextual information transparent throughout the programming effort. The model was built from first principles, every decision was rooted in the formative assumptions above, and every effort was made to ensure parsimony in terms of concepts and notation.

Algorithms for Mobility. Our group has also been active in the development of new algorithms for mobile computing. Some of the work is set in the base station mobility model, which is similar to the cellular telephone network with a set of fixed base stations that communicate with the mobile units as they move within a region. Nodes represent mobile base stations and channels represent the communication connections among these base stations. Interestingly, we found that it was possible and advantageous to treat mobile units as messages. We accomplished this by making a small adjustment in the handover protocol to give the appearance that mobile unit movement among base stations takes place in a FIFO manner. This strategy enabled us to convert traditional distributed algorithms to novel ones in the mobile environment. For example, we developed an algorithm for reliable multicast of a message to all mobile units in a region. The algorithm, based on the Chandy-Lamport distributed snapshot algorithm, has several attractive properties with respect to delivery guarantees in rapidly changing environments and network overhead. A second algorithm, based on the model of diffusing computations by Dijkstra and Scholten, has been developed to track the movement of a mobile unit within a region of base stations. With this tracking information, the broadcast of a message can be limited in range, involving less network traffic while still allowing for rapid mobile unit movement. Finally, we have explored algorithm development for a more extreme form of mobility: mobile ad hoc networks. As part of this effort, we developed an algorithm to detect termination of diffusing computations in a manner that is independent of network topology and tolerant of disconnection. An interesting feature of the algorithm is its reliance on the use of a logical network delivery structure induced by host activities and motion.

Coordination Middleware for Mobility. The LIME (Linda In a Mobile Environment) middleware provides a set of abstractions for enabling rapid development of dependable applications that exhibit physical mobility of hosts, logical mobility of agents, or both. LIME extends the Linda model of process coordination to allow tuple spaces to be distributed in time and space and transiently shared when connectivity is available. Movement, logical or physical, results in implicit changes to the contents of the tuple space accessible to the individual components. The system, not the application program, manages the movement of tuples and the tuple space restructuring associated with connectivity changes. LIME provides the application programmer with the standard set of Linda operations as well as a second set of operations dealing with the distribution of the tuples with respect to location. This expanded set of primitives allows the programmer to control the level of transparency of mobility depending on specific application needs. Several applications were developed to demonstrate the effectiveness of the LIME middleware in the development of mobile applications. LIME is available under an open source licensing agreement. A derivative of LIME, called Limone, offers a lightweight version of the original model better suited to accommodate transient interactions and limited resources typical of ad hoc networks. In a related middleware development, EgoSpaces facilitates rapid development of sophisticated context-aware applications by allowing applications to define contexts that reflect diverse concurrent and changing needs and encompass data from multiple sources. EgoSpaces manages this information for the application, relieving the developer from having to handle network connections and disconnections common in mobile environments. This work represents a significant step in creating a context-aware computing infrastructure targeted at simplifying the development of adaptive mobile applications. The main contributions of this model are: a redefinition of context-awareness in mobile environments, the elucidation of a programming model amenable to dynamic applications and tailored to a novice programmer's capabilities, and the implementation of a middleware that provides programming constructs that simplify the development of a large class of context-aware applications.

Secure Service Provision in Ad Hoc Networks. The emerging paradigm of Service Oriented Computing promises to change the way functionality is delivered to the end user. Our group has been the first to introduce service-oriented computing to the development of applications over ad hoc wireless networks. We used the Jini model as the basis for our framework and adapted it to handle the nuances of the ad hoc network. We employ a federated service directory that is distributed across the hosts that comprise the ad hoc network. Service providers advertise the existence of a service by placing an advertisement in the service directory. Interested users can perform a pattern search over advertisements in the service directory to discover services that they may require. A matching algorithm pairs requests to applicable advertisements. The basic framework has been enriched further by the addition of convenience features. A security veneer facilitates secure advertisement and discovery as well as encrypted communication between proxies and servers using well-known encryption standards such as DES and RSA. Additional capabilities include an automatic code management system to obtain binaries on demand to support the execution of the proxy, an upgrade system that provides the ability to modify the service as well as multiple instances of its proxy at run time in a manner that is transparent to the clients using the proxy, mobile threads that support migration of services and clients from one host to another, and a knowledge management system that exploits non-functional characteristics of the network to increase predictability in a volatile environment. Similar knowledge about the mobility profiles of individual hosts contributed to the development of a new class of protocols that support disconnected routing among hosts that are never in communication contact with each other. Finally it led to the design of mechanisms and policies that enable continuous service provision despite the physical mobility of hosts, rapid changes in the environment, and variability in the resources offered by the evolving ad hoc network.

Spatiotemporal Services in Sensor Networks. Sensor networks are an important new disruptive technology. Our first research efforts in this area addressed the issue of coordinated message delivery and led us to investigating a new variant of the traditional multicast called mobicast. The latter entails the delivery of messages to large sets of nodes in a manner that satisfies a potentially dynamic set of spatiotemporal constraints. In order to demonstrate the feasibility of mobicast, we proposed a new topology-aware routing protocol for sensor networks. Worst-case analysis shows that the protocol provides strong spatial and temporal delivery guarantees under reasonable assumptions about the network. The design of the protocol relies on new notions of compactness for spatially distributed networks. By explicitly addressing the temporal domain associated with message delivery, mobicast is more general than geocast and makes it possible to save precious resources in sensor networks by exploiting its inherent just-in-time delivery semantics. Furthermore, a protocol called Face-Aware Routing was developed to achieve reliable mobicast delivery in sensor networks that exhibit large gaps in sensor coverage. The key features of the protocol are a routing strategy, which uses information confined solely to a node's immediate spatial neighborhood, and a forwarding schedule, which employs only local topological information. Finally, we also developed two new wake-up and topology maintenance protocols (Directional Tree Maintenance and Omni-directional Tree Creation) to support spatiotemporal services in mobile environments. They have been shown to provide robust spatiotemporal performance while maintaining low overhead and energy consumption.