A survey of theories for mobile agents <s> Still other formalisms <s> My goal is to propose a set of questions that I think are important. J. Misra and I are working on these questions. <s> BIB001 </s> A survey of theories for mobile agents <s> Still other formalisms <s> We present a model of distributed computation which is based on a fragment of the π-calculus relying on asynchronous communication. We enrich the model with the following features: the explicit distribution of processes to locations, the failure of locations and their detection, and the mobility of processes. Our contributions are two folds. At the specification level, we give a synthetic and flexible formalization of the features mentioned above. At the verification level, we provide original methods to reason about the bisimilarity of processes in the presence of failures. <s> BIB002 </s> A survey of theories for mobile agents <s> Still other formalisms <s> 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. So far, the literature on mobile computing is dominated by concerns having to de with the development of protocols and services. This article complements this perspective by considering the nature of the underlying formal models that will enable us to specify and reason about such computations. The basic research goal is to characterize fundamental issues facing mobile computing. We want to achieve this in a manner analogous to the way concepts such as shared variables and message passing help us understand distributed computing. The pragmatic objective is to develop techniques that facilitate the verification and design of dependable mobile systems. Toward this goal we employ the methods of UNITY. To focus on what is essential, we center our study on ad hoc networks , whose singular nature is bound to reveal the ultimate impact of movement on the way one computes and communicates in a mobile environment. To understand interactions we start with the UNITY concepts of union and superposition and consider direct generalizations to transient interactions. 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 a certain range. The notation we employ is a highly modular extension of the UNITY programming notation. Reasoning about mobile computations relies on extensions to the UNITY proof logic. <s> BIB003 </s> A survey of theories for mobile agents <s> Still other formalisms <s> We introduce the spi calculus, an extension of the pi calculus designed for describing and analyzing cryptographic protocols. We show how to use the spi calculus, particularly for studying authentication protocols. The pi calculus (without extension) suffices for some abstract protocols; the spi calculus enables us to consider cryptographic issues in more detail. We represent protocols as processes in the spi calculus and state their security properties in terms of coarse-grained notions of protocol equivalence. <s> BIB004 </s> A survey of theories for mobile agents <s> Still other formalisms <s> In this paper we present a calculus of communicating systems which allows one to express sending and receiving processes. We call this calculus Plain CHOCS. The calculus is a refinement of our earlier work on the calculus of higher order communicating systems (CHOCS). ::: ::: Essential to the new calculus is the treatment of restriction as a static binding operator on port names. The new calculus is given an operational semantics using labelled transition systems which combines ideas from the applicative transition systems described by Abramsky and the transition systems used for CHOCS. The new calculus enjoys algebraic properties which are similar to those of CHOCS only needing obvious extra laws for the static nature of the restriction operator. ::: ::: Processes as first class objects enable description of networks with changing interconnection structure, and there is a close connection between the Plain CHOCS calculus and the ?-Calculus described by Milner, Parrow and Walker: the two calculi can simulate one another. ::: ::: Recently object oriented programming has grown into a major discipline in computational practice as well as in computer science. From a theoretical point of view object oriented programming presents a challenge to any metalanguage since most object oriented languages have no formal semantics. We show how Plain CHOCS may be used to give a semantics to a prototype object oriented language calledO. <s> BIB005
The formalisms described in this paper represent a quite limited selection among many other altogether useful approaches to formally describe concurrent and mobile systems. Mobility is now a major focus and new formalisms stressing the notions of locality, failure and security continue to be proposed. Plain CHOCS BIB005 ] is an intermediary calculus between π-calculus and HOπ in the sense that it enables processes to communicate through fixed channels. Processes are allowed to send other processes, but not names, through the channels. The configuration of processes is static (names are not allowed to be passed in the channels), but processes can change their behavior dynamically. The calculus of BIB002 ] is based on an asynchronous π-calculus and introduces the notions of explicit distribution of processes to locations, failure of locations, detection of failure locations, and mobility of processes. The join-calculus and the distributed join-calculus are extensions of the π-calculus which introduce the notion of named location and distributed failure. Locations form a tree of embedded locations, and locations can move from one location to another. Regarding the problem of coordination among mobile agents we mention LLinda [De Nicola et al. 1997a,b] which is a process calculi for multiple tuple spaces that also addresses security aspects. Security is also at the center of the spi-calculus BIB004 : this π-calculus extension was designed for the description and analysis of cryptographic protocols. An important aspect of all these formalisms is whether they can serve as a base for tools and for verification of properties. In  ] the π-calculus is modeled in terms of history-dependent automata (with local names in the transitions) that may lead to simpler and automatic validation procedures. Mobile UNITY BIB003 is an extension of UNITY BIB001 that augments the program state with a location attribute. Recently, this formalization of physical mobility has been used for expressing various forms of code mobility  ; program properties have been expressed and formally verified  ] using the UNITY proof logic.