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.
-
Control flow analysis [6] consists in capturing all the potential interactions between the agents of a system. It detects where names can be communicated in the system. Our analysis is precise enough to distinguish between recursive instances of the same agent. This way, it can be used in proving that the variables of an agent are always bound to names having being declatarget by the same recursive instance of this agent.
Such properties are crucial in proving the integrity of an ftp-server used by an unbounded number of clients.
- Occurrence counting analysis consists in counting the number of simultaneous instances of agents during computation sequences. In mobile ambients, we count the number of agents both inside each ambient and inside the whole system.
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.