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.
-
Control flow analysis [5] 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 channel names having being declared 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 [6] consists in counting the number of simultaneous instances of agents during computation sequences. It can be used in proving mutual exclusion between agents and the non-exhaustion of the resources used by a system.
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.