## PresentationPresentation Jury Abstract## DownloadThesis Report Slides Photos## PrototypesPrototypes## Analysis examplespi-calculus ambient calculus environment analysis occurrence counting analysis thread partitioning |

Analysis of mobile systems by abstract interpretation

Jérôme Feret

Defended the 25th of February 2005

École Polytechnique

This thesis has been done at Laboratoire d'Informatique of the École Normale Supérieure (Paris)

- PhD advisor
- M. Patrick
Cousot - President
- M. David
Schmidt - Reviewers
- M. Luca
Cardelli - M. David
Schmidt - Examiners
- M. Vincent Danos
- M. Roberto Giacobazzi
- M. Jean Goubault-Larrecq

A mobile system is a pool of agents that
may interact with each other.
These interactions dynamically change the system by controlling both creation and destruction of links between agents. These interactions also control the creation of new agents.
The size of a mobile system evolves during its computation. This size may be unbounded.
A mobile system may describe telecommunication networks, reconfigurable systems, *client-server* applications, cryptographic protocols, or biological systems.
Several models are available according to the application field and the granularity of the observation level.

In this thesis, we propose an unifying framework to discover and prove automatically and statically some properties of mobile systems. We propose a meta-language to encode the most current models for mobility (the

We then use the Abstract Interpretation framework to derive abstract semantics, which are sound, decidable, but approximate.
In this thesis, we give three generic semantics that we set according to the expected trade-off between accuracy and efficiency.
The first analysis focuses on dynamic properties: it captures relations about the creation histories of the agents of the system. This analysis is precise enough to distinguish recursive instances of each agent, even when there is an unbounded number of instances. Thus, we can prove in the case of a *client-server* application that the server always returns data to the right client.
The second analysis focuses on concurrency properties: it counts the number of occurrences of agents inside the system. This analysis detects mutual exclusion and it bounds the number of agents.
The third analysis mixes concurrency and dynamic properties. It gathers the agents of the system in several computation units. Then, it abstracts the number of occurrences of agents in each computation unit. For instance, we can prove the absence of race in the specification of a shared-memory with dynamic allocation that is written in the

- Slides of the 45mn presentation are available in various format:
- Slides of the presentation at PPS concurrency working group

Prototypes can be used on line (Computation are made on a

Analysis examples (These results have been computed on a

- Example 2.1.1: ftp server
- Example 2.1.2: token ring
- Example 2.2.4: toy example

- Example 3.1.1: ftp server (in ambients)

- Example 8.2.6: ftp server
- Example 8.2.7: token ring
- Example 8.2.8: server (in ambients)
- Example 8.2.11: causality
- analysis input
- analysis output (uniform analysis)
- analysis output (non uniform analysis)

- Example 9.4.1: ftp server
- Example 9.4.2: token ring
- Remark 9.4.3: token ring We do not count transitions in this example.
- Example 9.4.4: token-server in ambients

Only implemented for mobile ambients. For the pi-calculus, we give results of environment analysis.

- Example 10.1.1: shared memory The confidentiality proof requires the analyses proposed in Sect. 8.3, which are not implemented yet. Confidentiality can be infered for the simplified version of the example by using analyses proposed in Sect. 8.2. The absence of race conditions requires analyses proposed in Chap. 10, which are not implemented yet.
- original
- without context
- simplified
- Example 10.2.2: token-server in ambients