PoK

Authors: Gruia-Catalin Roman, Peter J. McCann

Description:
Traditionally, a distributed system has been viewed as a collection of fixed computational elements connected by a static network. Prompted by recent advances in wireless communications technology, the emerging field of mobile computing is challenging these assumptions by providing mobile hosts with connectivity that may change over time, raising the possibility that hosts may be called upon to operate while only weakly connected to or while completely disconnected from other hosts. We define a concurrent mobile system as one where independently executing components may migrate through some space during the course of the computation, and where the pattern of connectivity among the components changes as they move in and out of proximity. Note that this definition is general enough to encompass a system of mobile hosts moving in physical space as well as a system of migrating software agents implemented on a set of possibly non-mobile hosts. In this paper, we present Mobile UNITY, which is a notation for expresing such systems and a logic for reasoning about their temporal properties. Based on the UNITY language of Chandy and Misra, our goal is to find a minimalist model of mobile computation that will allow us to express mobile components in a modular fashion and to reason formally about the possible behaviors of a system composed from mobile components. A simplified serial communication protocol among components which can move in space serves as an illustration for the notation.

Authors: Gruia-Catalin Roman, Rose F. Gamble, William E. Ball

Description:
This paper describes a formal approach for developing concurrent rule-based programs. Specification refinement is used to generate an initial version of the program. Program refinement is then applied to produce a highly concurrent and efficient version of the same program. Techniques for deriving concurrent programs through either specification or program refinement have been described in previous literature. The main contribution of this paper consists of extending the applicability of these techniques to a broad class of rule-based programs. To the best of our knowledge, this is the first time formal derivation is employed in the context of rule-based programming.

Authors: Rohan Sen, Radu Handorean, Gregory Hackmann, Gruia-Catalin Roman

Description:
In the proxy approach to Service Oriented Computing, a service advertises a proxy, which is searched for, retrieved and used by interested clients as a local handle to the service process that runs on a remote host. Due to software evolution, it becomes necessary at times to upgrade the service. Some of these upgrades may require an upgrade of the proxy software, in addition to the server itself. This paper addresses the issue of upgrading both the server and its proxy in a manner transparent to the client, and ensures only momentary interruption during the switching process. The model we propose is designed for ad hoc wireless networks, but can be used in other settings as well. We also describe a Java implementation of our model.

Authors: Gruia-Catalin Roman, Gian Pietro Picco, Amy L. Murphy

Description:
The term distributed computing conjures the image of a fixed network structure whose nodes support the execution of processes that communicate with each other via messages traveling along links. Peer-to-peer communication is feasible but client-server relationships dominate. More recently, servers have been augmented with brokerage capabilities to facilitate discovery of available services. Stability is the ideal mode of operation; changes are relatively slow; even in the case of failure, nodes and links are expected eventually to come back up. By contrast, mobility represents a total meltdown of all the stability assumptions (explicit or implicit) associated with distributed computing. The network structure is no longer fixed, nodes may come and go, processes may move among nodes, and even programs (the code executed by processes) may evolve and change structure. The challenges and opportunities associated with this computational melee form the main subject of this paper. We seek to sort out this chaotic form of computing by focusing our attention on the formulation of a simple framework for viewing mobility, on precise definition of terms, and on research issues mobility poses for the software engineering community.

Authors: RAJEEV ALUR, THOMAS A. HENZINGER, GERARDO LAFFERRIERE, GEORGE J. PAPPAS

Description:
A hybrid system is a dynamical system with both discrete and continuous state changes. For analysis purposes, it is often useful to abstract a system in a way that preserves the properties being analyzed while hiding the details that are of no interest. We show that interesting classes of hybrid systems can be abstracted to purely discrete systems while preserving all properties that are definable in temporal logic. The classes that permit discrete abstractions fall into two categories. Either the continuous dynamics must be restricted, as is the case for timed and rectangular hybrid systems, or the discrete dynamics must be restricted, as is the case for o-minimal hybrid systems. In this paper, we survey and unify results from both areas.