Ad Hoc & Sensor Network Software (2005 - Present)

Agent Systems for Sensor Networks Agilla is a middleware designed to enhance our ability to program applications for wireless sensor networks.  It is the first mobile agent middleware that works in the resource-constrained environment of a sensor network.  Mobile agents offer both code and state mobility.  Because they can migrate across the sensor network, multiple applications can co-exist in the same sensor network, new applications can to be injected, and existing applications can adapt.  Agilla's underlying context discovery and coordination primitives consist of a neighbor list and a tuple space.  They facilitate inter-agent communication while maintaining each agent's autonomy and providing a rich infrastructure for building sophisticated applications.  Agilla has been implemented on Mica2, MicaZ, and Tyndall 25mm sensors and has been integrated with the Cricket indoor localization system.  Agilla's implementation consumes a mere 41.6KB of code and 3.59KB of data memory.  Mobile agents can migrate 5 hops in less than 1.1s with over 92% reliability.  Agilla was evaluated on multiple test applications related to fire detection and tracking, cargo container monitoring, robot navigation, intruder detection and tracking, and network exploration.  Most importantly, Agilla introduced a promising new programming paradigm to the field of sensor networks facilitating an unprecedented degree of programming flexibility.

Mobile Computing (1995 - 2005)

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.

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.

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 light weight 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.

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.

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 builtfrom 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.

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.

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.

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.

Program Visualization (1990 - 2000)

I founded the Computer Visualization Laboratory as a research facility whose mission was to investigate methodologies for integrating computing and visualization, to explore technologies that make feasible the fusion of the two disciplines, and to provide video production and multimedia capabilities for use in research and instruction. Our research on program visualization made possible rapid visualization of program executions, reduced (and often completely eliminated) the need to access the program code when building a visualization, offered unprecedented expressive power with minimal notation, and provided several capabilities important to the introduction of program visualization into the industrial setting.  The key technical contribution that enabled us to achieve these goals was the notion of declarative visualization, embodied in the design of a visualization system called Pavane.  The declarative paradigm treats visualization as a mapping from program states to animated three-dimensional scenes.  An extensive evaluation of Pavane in a wide range of settings (formal design, distributed algorithms, scientific visualization, requirements validation, monitoring, debugging, etc.) showed that complex animations of system behaviors can be constructed within three to six hours, often using less than two dozen declarative rules.  In addition, Pavane offers a broad range of navigational capabilities to viewers and animators as well as through-the-screen interactions.  An interesting byproduct of this work was the development of a proof-based visualization methodology, an approach that exploited formal proofs of concurrent programs to guide the choice of graphical representation and associated animations.

Formal Design Methods (1985 - 1995)

An important goal of my research has been the industrial application of formal design methods, i.e., methods that have a primarily mathematical rather than empirical foundation.  Design methodologies play a critical role in this process by shaping the body of knowledge designers must acquire, the skills they need to master, and the kinds of tools they might employ.  In my group, we viewed program derivation (in its many forms) as the principal venue for the study and development of formal design methods.  Because we wanted to bridge formal studies and industrial practice, we explored program derivation techniques that were amenable to both formal and semi-formal application.  Because we sought to uncover and understand fundamental issues facing concurrent systems design, the models we employed exhibit parsimony and extensions to these models were kept to a minimum. Our investigation into formal design methods centered on the UNITY model (proposed by Chandy and Misra) and was directed towards extending the applicability of various program derivation techniques to novel design domains.  Refinements of the UNITY notation and logic, new program derivation strategies, and detailed case studies have been the principal technical results of this investigation. The relation between systematic (but informal) design practices and the UNITY-style specification refinement was studied in the context provided by the design of a message router. In an attempt to overcome the static features of UNITY we developed a highly dynamic variant called Swarm.  The two models share a common proof logic but the static variables and statements of UNITY were replaced in Swarm by dynamically created tuples and transactions over tuple spaces.  Swarm facilitated the introduction of formal verification and derivation techniques to tuple-based languages à la Linda and to rule-based systems à la OPS5.  Several case studies involving the derivation of programs meant to execute on specific kinds of parallel or distributed architectures led to the development of an assertional-style technique for formal specification of architectural constraints and to the emergence of a new program derivation strategy that integrates specification and program refinement.  Swarm was also instrumental in the study of methods for specifying and reasoning about dynamic forms of synchrony among atomic actions.

Early Work (1975 - 1990)

Software engineering has been a central theme of my research throughout my career.  The starting point was my dissertation, which demonstrated the potential for dependability and productivity improvements through systematic use of formal methods.  Nevertheless, my early research spanned a broad range of investigative domains including biomedical simulation, formal languages, distributed databases, computer graphics, and image understanding.  Some of the most interesting results have been those stemming from fruitful collaborations with colleagues in the department:  one of the first fully distributed algorithms for concurrency coordination in distributed databases, a novel pipelined architecture for real-time hidden surface elimination, a logic-based model for geographic data processing, and algorithms for real-time stereo matching.