Contents Next

1   Introduction

In a mobile system, agents can be dynamically created and then communicate some data to others agents. These communications dynamically change the topology of the interactions between agents. This makes the analysis of mobile system a very difficult task. The p-calculus [9, 8] is a well-fitted model of mobile systems. It deals with agents which declare fresh channel names and then communicate them to other agents. Names provides some control over other agents: when an agent receive a name, it can use it to send other names to another agent via this name. This encodes mobility.

We describe here the implementation [4] of two previously proposed analyses [5, 6]. These analyses automatically infer a sound description of the potential behaviour of a mobile system written in the p-calculus. Our analyses are context free: the system can interact with an unknown context. We use the Abstract Interpretation framework [2, 3] 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 two examples: the token-ring and an ftp-server. The token-ring is a mobile system which recursively creates a ring of processes, then a token is given to the first process of the ring. When having the token, a process first computes its thread then passes the token to the next process of the ring. Our tool discovers that a process can only be connected to the next process of the ring, and that only one process can be computed in the same time. The ftp-server is a mobile system which describes the behaviour of a server which can been used by an unbounded number of clients. Nevertheless for physical restriction, this server cannot establish more than three simultaneous sessions. Our tool will be used in validating this mobile system, by proving that the answer of a client's query can only be communicated to the client which has sent this query and by proving that no more than three sessions can been simultaneously run.

In Sect. 2 we describe the standard semantics of the p-calculus, 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