Contents Next

1   Introduction

Mobile ambients [1] are a model of mobile computation. It describes a set of agents which are distributed throughout hierarchically organized domains called ambients. Agents interact inside ambients which makes the ambients move, taking with them their content. Thus mobility is described explicitly.

We describe here the implementation [5] of several analyses. These analyses automatically infer a sound description of the potential behaviour of a mobile system written in mobile ambients. We use the Abstract Interpretation framework [3, 4] to solve problems due to undecidability. We focus of two classes of properties: we analyze both the control flow and the occurrence number of agents.

We will illustrate our implementation by giving an example of an ftp-server with an unbounded number of clients. Our analyzer proves that information cannot be returned to the wrong client.

In Sect. 2 we describe the standard semantics of mobile ambients, in Sect. 3 we refine this semantics in order to take into account the link between recursive instances of agents, and the names they declare. In Sect. 4, we describe what our tool calculates. In Sect. 5, we interpret the results obtained with our examples and in Append. A, we shortly explained available options for the analysis.

Contents Next